What does ALASKA mean ?

Antichains for Logic, Automata and Symbolic Kripke structure Analysis.

How stable / well-tested is the implementation ?

ALASKA is a very early prototype. It has neither been tested extensively, nor been largely distributed (yet). Keep that in mind when interpreting results of the tool. Still, to our knowledge, ALASKA is pretty accurate and trustable (for a first prototype).

How fast is ALASKA ?

On a large set of examples, we have observed that ALASKA is several orders of magnitude faster than NuSMV for both LTL satisfiability and model checking. See the experiments Section for more information.

What's with the bubbles ?

The ALASKA logo represents an antichain. The top bright-colored bubbles are the "maximal" elements w.r.t. a simulation preorder, and the light, smaller bubbles represent the subsumed elements.

Why is NuSMV needed for model checking ?

NuSMV is used for parsing SMV specifications and dumping BDD-encoded Kripke structures to a text file. The patch from the download section adds a command "bddfsm2file" to the NuSMV interpreter which implements the dumping procedure. ALASKA reads those dumpfile to perform model checking. Note that dumping and reading large Kripke structures is time consuming, and those times should not be taken into account when evaluating ALASKA's performance.