Experimental Results
We have tested extensively our tool against the performances of NuSMV. For testing the satisfiabily of LTL formulas, Alaska performs generally much better than NuSMV. For model-checking, the gain in performance appears mainly when the size of the LTL formulas grow. You can find here the results of those experiments. Be aware that some of the scales on the time axis are logarithmic. More details can be found in:
- Martin De Wulf, Laurent Doyen, Nicolas Maquet, Jean-Francois Raskin. Antichains: Alternative Algorithms for LTL Satisfiability and Model-Checking. Proceedings of TACAS 2008, LNCS, Springer-Verlag, Budapest, 2008.
Nevertheless, the figure on this site are different from the ones in the paper, since the Alaska tool has been updated since the publication of the paper.
All input files are available for download
LTL Satisfiability
Lift Formulas
The first family is a parametric specification of a lift system with n floors that we have taken from Harding's thesis. Two encodings are used: one ("lift") that uses a linear number of variables per floor, and another ("lift-b") which uses a number of variables that is logarithmic in the number of floors (resulting in larger formulas).
Szymanski Formulas
The second family of formulas was referenced in an article by Sebastiani, Tonetta and Vardi in 2005 as examples of difficult LTL to NBW translation and describes liveness properties for the Szymanski mutual exclusion protocol and for a variant of this protocol due to Pnueli.
Counter Formulas
Finally, the last set of formulas describes how a binary counter, parameterized by its length, is incremented. Two ways of formalizing the increment are considered (``count", ``count-l"). Those formulas are quite particular as they all define a unique model: for n=2, the model is [00 ... 01 ... 10 ... 11]*. In this benchmark, the classical fully-symbolic algorithm behaves much better than our antichain algorithm. This is not surprising for two reasons. First, the efficiency of our antichain-based algorithms comes from the ability to identify prefixes of runs in the ABW which can be ignored because they impose more constraints than others on the future. As there is only one future allowed by the formula, the locations of the NBW defined by the Miyano-Hayashi construction are incomparable for the simulation relation, causing very long antichains and poor performances. This can be considered as a pathological and maybe not very interesting case.
Model Checking
Gas Station
This family describes a gas station with an operator, one pump, and n customers (n is a parameter) waiting in line to use the pump. The operator manages the customer queue and activates or deactivates the pump. This resource-access protocol was used in a paper by Sebastiani, Tonetta and Vardi in 2005 as an LTL model-checking benchmark. We have used the same LTL formulas as them.
Bakery Algorithm
This family of models is a finite state version of the Lamport's bakery mutex protocol. This protocol is interesting becauses it imposes fairness among all processes and again it is parametric in the number n of participating processes. Our model is large and grows very rapidly with the number of processes. For 2 processes, it uses 42 boolean variables and requires BDDs with a total of 7750 nodes to encode the model, for 4 processes, it uses 91 variables and BDDs with more than 20 million nodes.
Note that when there is no data drawed for a size of the model, it means that the tool did not succeed in finishing the model checking.
Stack
This family of models also comes from the same paperand represents a stack, on which push, pop, empty and freeze operations can be performed. Each cell of the stack can hold a value from the set {1,2} and a freeze operation allows to permanently freeze the stack, after which the model runs a pointer along the stack from top to bottom repeatedly. At each step of this infinite loop, a ``call'' predicate indicates the value currently pointed. For example, if the stack contains, from bottom to top, {1,2} then after the freeze operation, the model will behave like this : call2, call1, call2, call1, ...} As we needed a scalable set of formulas for at least one model to compare the scalability of our algorithm with NuSMV, we have provided and used our own specifications for this model. These specifications simply enforce that if the sequence of push operations "12 ... n" is performed and not followed by any pop until the freeze operation, then the subsequence of call operations "n ... 21" appears infinitely often.
