Experiments for CAV 2006

This page contains the implementation and files related to the experiments performed in the paper "Bounded Model Checking for Weak Alternating Buchi Automata" by Keijo Heljanko, Tommi Junttila, Misa Keinänen, Martin Lange, and Timo Latvala.

The Implementation

UPDATE 16.4.2007: We are now able to distribute the sources of our modified version of NuSMV. The package requires either Minisat or zchaff in order to compile. The previously distributed binary is still available below. Download the sources from here:

NuSMV-CAV2006.tar.gz

The package below contains a Linux (x86) binary of a development version of NuSMV with our incremental SAT technology and new encodings integrated. The binary has been tested on Debian's stable distribution. The NuSMV binary is statically linked to the SAT solver zchaff, version 2004.11.15. The use of zchaff is restricted by the following license:

http://www.princeton.edu/~chaff/zchaff/COPYRIGHT .

The binary of the modified version of NuSMV bcan be downloaded here (use 'Save Link As'):

NuSMV.gz

The NuSMV binary also contains a statically linked version of Minisat, which is governed by the following license:

http://www.opensource.org/licenses/mit-license.php .

Our bounded model checking package for PSL specifications is used like the standard BMC package for LTL, with the exception that you should use the command 'check_pslspec_bmc' instead of 'check_ltlspec_bmc'. The command for using our implementation of the Miyano-Hayashi algorithm is 'check_pslspecmh_bmc'. By issuing the command 'set waba_buchi', the command 'check_pslspec_bmc' will first translate the WABA to a Buchi automaton, which is then used for BMC. This is inactivated with command 'unset waba_buchi'. The degree of unrolling for the waba encoding can be set with the command 'set waba_unroll X', where X is an integer. With X=0, the algorithm does full unrolling, and values larger than zero specify the number of unrollings.

We have also implemented an interface that allows weak alternating automata to be used as specifications instead of PSL. The command is 'checkspec_cav2006_bmc -f filename' where 'filename' contains the automaton. If the given automaton is not a WABA, an error is reported. The command also reports whether the WABA is very weak. We have implemented a simple python script that generates random WABAs: wabagen2.py .

Please note that all PSL properties must be supplied at the command line with the option '-p'. We do not currently support the PSLSPEC directive in NuSMV models. Due to an unknown problem in the tool chain, some PSL properties are not correctly translated: the resulting WABA is not equivalent to the given PSL property.

Experiments

We use a simple Perl script to generate the random Kripke structures for the experiments.

randomKripke.tar.gz

LTL Experiments

The random formulas that are the data for generating Figures 1(a), 1(b) and 1(c) are in this package: ltl_formula.tar.gz A simple script for running the experiments is this: runtest2.sh. The script will require simple modifications such as directories in order to run.

PSL Experiments

The random formulas that are the data for generating Figures 2(a-f) are in this package: ltl_form.tar.gz A slightly more sophisticated script is used to run the experiments, as only the subset of PSL formulas that generate non-very weak alternating automata is used. The script is included in the package, and it requires that that the subset of formulas is given.

Generating Plots

For generating the plots, and analysing the results the following collection of scripts is useful: plot_scripts.tar.gz

Timo Latvala,