Thesis

Here you can find my (unrevised) thesis. The short version is available too.

Good-for-Games

Usage of LTL-To-G4G

As prerequisite we assume that you have ltl2ba and ltl2dstar installed. For the GFG automata generation, please download and compile ltl-to-g4g. For this, execute in the directory the following:

tar xzf ltltog4g.tar.gz
cd ltltog4g/build
cmake ../src
make

Now, the binaries ltl2dstar-to-bdd and ltl-to-g4g should be in the current path (build/). ltl2dstar-to-bdd and ltl-to-g4g expects you to have ltl2ba in the same directory. Additionally, ltl2dstar-to-bdd expects you to have ltl2dstar in the same directory. You can create symbolic links. ltl-to-g4g and ltl2dstar-to-bdd supports an --ltl flag, which allows to supply an LTL formula in prefix format:

ltl-to-g4g --ltl 'U p0 G p1'

Both programs share also the following BDD-related flags:

Additionally, ltl2dstar-to-bdd supports an -O flag, which redirects the flag to ltl2dstar. E.g.,

ltl2dstar-to-bdd -O --bisimulation=no --ltl 'U p0 G p1'

disables bisimulation (in ltl2dstar). The following flags supported by ltl-to-g4g are important to follow the thesis:

Using PRISM with LTL-To-G4G

To follow the experiments on GFG-based analysis in PRISM, please download our extended prism and compile it with make. We recommend you to use solely make and not some multi-threaded variant, as some problems can occur. make creates some symbolic links in bin/ to ltl-to-g4g, ltl2ba, ltl2dstar and ltl2dstar-to-bdd, which may be incorrect and should be redirected in this case. The following flags are supported by PRISM:

For example, to use GFG-based analysis with dynamic reordering and the union construction in LTL-To-G4G and memory bound of 10G for CUDD, execute

bin/prism -ltlmethod g4g -allpathltl -mtbdd -g4goptions --dynamic-reorder=1 -g4goptions --dynamic-reorder-timeout=100 -g4goptions --union=1 -cuddmaxmem 1073741824 <model> <property-file>

Benchmarks

We have packed the models and the formula in g4g-benchmark.tar.gz. In subdirectory prism/wlan we placed the models and the properties for the IEEE 802.11 case study. The models prism/wlan/models/wlan1.nm to prism/wlan/models/wlan6.nm are the model with the constant MAX_BACKOFF set to 1 (wlan1.nm) up to 6 (wlan6.nm). The properties Pr^min(φ_i) can be found as file prism/wlan/properties/wlani.nm.

The directories for the dining philosophers benchmark are structered similarly. As we considered only one model, it can be found under prism/din_phil/model/phil_lss3.nm. All properties are listed in prism/din_phil/properties/benchmark.props.

Unambiguity

Generate UBA

As our Markov chain analysis does not rely on any specific LTL-to-UBA translation, we recommend SPOT and its tool ltl2tgba to generate UBA from LTL formula.

As first step, download SPOT and compile and install it:

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

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

This will install the Spot binaries into spot-2.6.1/bin. For our purposes, we are interested in spot-2.6.1/bin/ltl2tgba. To try it out, execute

$ spot-2.6.1/bin/ltl2tgba -f 'F G a' -H -B -U

This will create a Büchi automaton (via -B) that is in HOA format (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 with UBA

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

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:

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-to-UBA generator.

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

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

and then invokation of 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.

Using PRISM with CY95

To use the automataless method for Markov chain analysis within PRISM, please download this extended version of PRISM. This automata-less method is also called PRISM CY95, e.g., in Section 4.2.2. To compile it, 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.8 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

PRISM CY95 adds one new flag to standard PRISM: --cy95. This flag asks PRISM to use the iterative rewrite method described by Courcoubetis and Yannakakis. As this method does not use any automaton at all, no external LTL-to-automata program is needed. Please remind, that the CY95 method works only on discrete-time Markov chains, and not on Markov decision processes. We support both the explicit engine and the hybrid engine. For example, to model check the dice model of Knuth with the property P=? [ F G s=7] in the hybrid engine, use the following command-line (in a single line)

$ prism/bin/prism -hybrid --cy95 prism-examples/dice/dice.pm -pf 'P=? [F G s=7]'

Instead of automata sizes, PRISM CY95 outputs the size of the last Markov chain in the iteration/rewrite process. The line in the output begins is

Transformed model has $n$ states.

where n is the number of states in the last Markov chain.

Benchmarks

We have packed all necessary models and properties as well as the automata in a benchmark archive. Please unpack this archive with a standard tar xzf uba-benchmark.tar.gz.

Bounded Retransmission Protocol

You can find the model in uba-benchmark/brp/model/brp.pm To specify the BRP model parameters, use

-const 'N=16,MAX=128'

as a PRISM parameter.

The properties can be found in uba-benchmark/brp/properties/. In particular, the properties are gathered in brp.pctl. This file includes the necessary PRISM properties for checking the LTL formula and for checking the automata 𝒜^k and ℬ^k. The automata themselves can be found as hoa-files. The filenames encode the specific automata: If the filename starts with det, it contains a deterministic automata. If the filename starts with uba, it contains a UBA. After this first part, there may be a cyclic, which means the automaton represents the cyclic variant, i.e., represents ℬ^k as in Section 4.2.2. Then a number follows, which encodes the k, i.e., the automaton represents the “k steps before”-pattern.

Complete and nearly-complete automaton

The directory uba-benchmark/complete-and-nearly-complete contains the necessary files for the benchmark detailed in Section 4.2.1. At first you need to generate the models and automata with generate-all. Then, 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 uba-benchmark/nba-vs-uba/all.ltl contains the LTL formulas used in Section 4.2.3, 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

Logs

You can find the logs here. The directory structure mimics the structure of uba-benchmark.tar.gz. The directory uba-logs/complete-and-nearly-complete contains the two log files for the experiments in Section 4.2.1 with log.qrdecomp standing for the QR Decomposition/the rank-based method and log.ubapower for the iterative, power-based method. The log files in uba-logs/brp contains the log files for the experiments in Section 4.2.2, the filename have the structure prism-method.log. Please note, that prism-uba.pure.log contains the log for the UBA-based methods without UFA-recognition and in case of a UFA, a simplified model checking process.

Emerson-Lei

Delag

Delag is now a part of Owl, a library for LTL and omega-automata. You can find the newest version of Delag here.

To obtain the version on which was used in the doctoral thesis, please unpack this tar.gz file. Please note the README file in the top directory (and ignore the README.md file). Independently of the version you use, you can translate an LTL formula by giving them just as a parameter:

./delag '(F G a) | (F G b)' 

LTL formulae

For your convenice, we have also added the LTL formulas. The mapping of the files is as follows:

Please note, that these formula are in prefix normal form of LBT. You can convert them using SPOT. For example, to convert | F G a F G b please use:

ltlfilt --full-parentheses --lbt-input --unabbreviate="MRW" -f '| F G a F G b'

PRISM

Our PRISM implementation based on PRISM 4.3.1 dev can be found here. To compile PRISM change into the prism/prism subdirectory and run make. A binary prism will be placed in prism/prism/bin To execute PRISM, we refer to README file contained in the top directory.

PRISM material

The material for PRISM can be found here. It contains the IEEE 802.11 model (wlan/model/wlan2.pm) and the properties (wlan/properties/wlanX.pctl). Please note, since we reused some properties for maximal and minimal probabilities, the mapping is as follows:

Logs

We provide the logs. The logs for the PRISM experiments are in el-logs/wlan/. The files separate the experiments by the different tools: