This website has some supplementary material to the paper “Markov Chains and Unambiguous Büchi Automata”.

Files

The website contains the following files:

Compilation and Installation

Compiling PRISM

To execute PRISM first download our extended version here, and unzip it via

$ tar xzf prism-uba.tar.gz

To compile PRISM, go to the prism/ subdirectory and execute ‘make’:

$ cd prism
$ make

This will work on Mac OS X and Linux and requires a Java JDK >=1.7 and the usual build tools (C/C++ compiler etc) to be installed.

If you have trouble compiling PRISM, please try downloading a source distribution from [http://www.prismmodelchecker.org/download.php] and try whether that works. We also refer to

[http://www.prismmodelchecker.org/manual/InstallingPRISM/CommonProblemsAndQuestions]

It might be necessary to set the JAVA_DIR variable so that the Makefile can find the JDK installation (see the Makefile): $ make JAVA_DIR=xxx

Additionally, don’t run make multi-threaded, i.e., with -j x for x>1.

As a result, you should have a working command-line version in

prism/bin/prism

and a GUI version in

prism/bin/xprism

Compiling Spot / ltl2tgba

If you want to try out the automatic handling of LTL formulas via an external LTL->UBA translation, please install Spot:

1. Download

[https://www.lrde.epita.fr/dload/spot/spot-2.7.tar.gz]

2. Compile & install

In case of difficulties, please consult [https://spot.lrde.epita.fr/install.html]

$ tar xzvf spot-2.7.tar.gz
$ cd spot-2.7
$ ./configure --prefix=`pwd` --disable-shared --enable-static --disable-python
$ make
$ make install

This will install the Spot binaries into spot-2.7/bin. For our purposes, we are interested in spot-2.7/bin/ltl2tgba

3. Try it out

   $ spot-2.7/bin/ltl2tgba -f ‘F G a’ -H -B -U

will create a Büchi automaton (via -B) that is in HOA format ([http://adl.github.io/hoaf/]) (via -H) and that is unambiguous (via -U) for the formula “eventually always a”.

By default, ltl2tgba will attempt an opportunistic determinization pass for formulas that are WDBA (weakly deterministic Büchi automata) realizable. To disable this determinization optimization and get “pure” UBA use the flag

-x wdba-minimize=0

Using PRISM-UBA

To use our version of PRISM with UBA-based model checking, you have two options. The first is to use a given UBA-HOA-file as the path formula.

As an example, try the following in the directory containing this README file:

$ prism/bin/prism -explicit -ltluba -ubaverbosity 1 prism-examples/dice/dice.pm -pf 'P=?[ HOA: {"FGa.uba.hoa", "a" <- s=7 }]'

This selects (1) the explicit engine, the only engine of PRISM where UBA PMC is currently implemented, (2) specifies that we want to use UBA PMC (-ltluba flag), (3) loads the dice.pm model file (Knuth’s dice example) and checks against the FGa.uba.hoa automaton, replacing the atomic proposition in the automaton with the state formula s=7, i.e., the success state of the model. Additionally, it selects a verbosity setting of 1 for the UBA PMC to provide some interesting information.

The FGa.uba.hoa file is located in prism-examples/dice, i.e., the path inside the HOA: ... specification is relative to the directory of the model file.

Additional substitutions of automata APs can be used for automata with more APs. If the substitution is not specified, e.g.,

P=?[ HOA: {"FGa.uba.hoa"}]

then each AP is connected with a label in the PRISM model of the same name.

Additional options for UBA-PMC:

-ubapure

Deactivates the special handling for the case where the UBA is (1) deterministic or (2) where the UBA is essentially an upward-close UFA, i.e., all F states have true loop. With this option, the full UBA algorithm is used, without it the standard PRISM handling for deterministic automata is used in case (1) and for (2) the SCC handling/positivity check and cut generation is skipped.

-ubapower

Activates the power iteration method for SCC handling, which can be significantly faster than the rank-based method.

-ubaposmethod svd | qr

For the rank-based SCC handling, use singular value decomposition (svd) or QR decomposition (qr) for the rank computation.

-ubareachmethod gs | colt

For the reachability part of the UBA algorithm, use the Gauss-Seidel algorithm (as used in PRISM) or use the COLT matrix library. Gauss-Seidel usually outperforms COLT.

For additional, standard PRISM settings we refer to [http://www.prismmodelchecker.org/manual/]

Of interest might be:

Besides HOA based model checking, PRISM-UBA also supports the use of ltl2tgba as an external LTL->UBA generator.

This requires (1) to set the path to the ltl2tgba executable as an environment variable:

$ export LTL2TGBA=path-to-spot-2.7/bin/ltl2tgba

Alternatively you can edit the invocation script prism/etc/scripts/hoa/hoa-ltl2tgba-uba-for-prism directly and set the LTL2TGBA variable there.

After setting LTL2TGBA you can use PRISM with the -ltl2datool parameter. As an example (in a single line):

$ prism/bin/prism -explicit -ltluba -ubaverbosity 1 -ltl2datool prism/etc/scripts/hoa/hoa-ltl2tgba-uba-for-prism -ltl2dasyntax lbt prism-examples/dice/dice.pm -pf 'P=?[ F G s=7 ]'

This will translate the LTL formula “F G s=7” into an UBA and perform model checking.

You can set

$ export LTL2TGBA_NOWDBA=1

to disable the WDBA minimization of ltl2tgba, i.e., to obtain UBA in more cases.

Benchmarks

To follow our benchmarks, please download our models, automata and formulas and unpack it with

$ tar xzf data.tar.gz

BRP

You can find a lua script generate-aut.lua in benchmark/brp/. It generates automata (𝒜 and ℬ in the paper) accepting the language ‘k steps before L0 happens, L1 must occur’ in the HOA format. You need a working lua interpreter to run this script (e.g. from [http://www.lua.org/download.html] or your distribution).

The script accepts two options and need a numeric parameter. The option --cyclic generates a cyclic automaton looping back after the “k-step” pattern has been consumed (B in the paper), otherwise generates the automaton A in the paper. The option --uba generates a UBA, otherwise generates the DBA. For example, the command line

$ lua generate-aut.lua --uba 34

generates a UBA with “34 steps before the first L0 occurs, L1 has to occur” as accepted language.

The file benchmark/brp/brp.pctl contains PRISM formulas for selected values of k for running against the model benchmark/brp/brp.pm

For taking an automaton as property, one has to generate it at first and save it, e.g., by

$ lua generate-aut.lua --uba 34 > uba.hoa

The corresponding property would be

P=?[HOA:{"uba.hoa", "L0" <- "L0", "L1" <- "L1"}]

Note the labelling assignment for correct translation of atomic propositions in the UBA to the atomic propositions in the DTMC.

To specify the BRP model parameters, use

-const 'N=16,MAX=128'

as a PRISM parameter.

Complete and nearly-complete automaton

The directory benchmark/complete-and-nearly-complete contains the necessary files for the benchmark detailed in Section 7.2.

M1.pm is the DTMC, the *.props files contain the property, the *.hoa files the generated automata. The script run-benchmark can be used to start the PRISM runs via the prism-auto script.

LTL formulas for the NBA vs UBA comparison

The file benchmark/nba-vs-uba/all.ltl contains the LTL formulas used in Section 7.4, in LBT format (prefix notation).

ltl2tgba needs the --ltb-input parameter to parse the formulas in this format.

For UBA, use the ltl2tgba parameters -U -B -H -x wdba-minimize=0 and for NBA use -B -H -x wdba-minimize=0