This website has some supplementary material to the journal paper “From LTL to Unambiguous Büchi Automata via Disambiguation of Alternating Automata” (FMSD 2020). You can find the supplementary material website for the conference version here.

Tool compiling and installation

Duggi

Duggi is an LTL to UBA translator that implements the construction in our paper. You can download the source files here.

To install, first make sure you have installed the following on your machine:

• cudd (We use version 3.0.0)
• boost (We use version 1.68)

Then follow the instructions in README.md to build the tool.

The executable duggi will be in the directory build. To see its options, type

$ build/duggi --help

which prints:

 $ General options:
 $   --help                 Show help message
 $   --formula arg          LTL formula in prefix syntax
 $   --verbose              Shows additional information in a comment
 $   --debug                Shows additional debug information in a comment
 $ 
 $ Automata options:
 $   --vwaa                 Show VWAA
 $   --gba                  Show generalized Büchi automaton
 $   --u                    create unambiguous automata
 $   --ba                   Show Büchi automaton

All automata are outputted in the HOA format, although we use empty successor sets in alternating automata which are currently not supported by the HOA format. You can manually make it compatible to other HOA tools by adding an additional state with a self-loop inducing the language Σ^ω and create an edge from a state with an empty successor set to this new state. The option --u tells duggi to make all automata unambiguous. For example, to see an unambiguous Büchi automaton for the formula ◇□a, type:

$ ./build/duggi --u --ba "F G a"

which prints:

$ HOA: v1
$ States: 3
$ Start: 0
$ AP: 1 "a"
$ Acceptance: 1 Inf(0)
$ --BODY--
$ State: 0 "(aut_index: 0) ( 0, { 4 } )" 
$ [t] 1
$ [t] 2
$ State: 1 "(aut_index: 1) ( 0, { 0 } )" 
$ [t] 1
$ [!0] 2
$ State: 2 "(aut_index: 4) ( 1, { 1 } )"  { 0 }
$ [0] 2
$ --END--

Additionally to the above mentioned flags, duggi offers the following hidden options:

 $   --no_unu_opt           turn u-nu-optim off
 $   --no_unamb_rewrites    turn simplifier_distributivity_unamb off
 $   --no_vwaa_opt          turn the GF f -> GXF f optimization off
 $   --choice_order         specifies the complementation state choice order

For choice_order you give a comma-seperated sequence of choices with the highest priority at first and lowest priority at last. They corresponds to the Section “Complementation state choice” in Section 3:

PRISM with UBA

At first step, please download our PRISM implementation and unzip it via

$ tar xzf prism-uba.tar.gz

To compile PRISM, go to the prism-uba/prism/ subdirectory and execute make:

$ cd prism-uba/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-uba/prism/bin/prism

and a GUI version in

prism-uba/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-uba/prism/bin/prism -keepAPs -explicit -ltluba -ubaverbosity 1 prism-uba/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-uba/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 our experiments, we did not use -ubapure, but -ubapower and -ubareachmethod gs, and for the BRP experiment, -keepAPs. 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 duggi and ltl2tgba as an external LTL-to-UBA generator. For this, one can use the switch -ltl2datool with according predelivered scripts, that can be found in the directory prism-uba/prism/etc/scripts/hoa/. The two important scripts in this directory are hoa-duggi-uba-for-prism and hoa-ltl2tgba-uba-for-prism. Before using them, please edit them and change the according paths to the binaries.

As an example for using duggi (in a single line):

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

Analogously for ltl2tgba:

$ prism-uba/prism/bin/prism -explicit -ltluba -ubaverbosity 1 \
   -ltl2datool prism-uba/prism/etc/scripts/hoa/hoa-ltl2tgba-uba-for-prism \
   -ltl2dasyntax lbt \
   prism-uba/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 DUGGI_NOWDBA=1

or

$ export LTL2TGBA_NOWDBA=1

to disable the WDBA minimization of duggi or ltl2tgba, i.e., to obtain UBA in more cases. You can do it both in the prism-uba/prism/etc/scripts/hoa/hoa-duggi-uba-for-prism (vs. prism-uba/prism/etc/scripts/hoa/hoa-ltl2tgba-uba-for-prism) scripts or on the commandline.

Experiments

In our paper, we compare our construction with the LTL to UBA generation of SPOT’s tool ltl2tgba. It can be downloaded together with the SPOT tool set.

LTLstore

We use the ltlstore to provide us with LTL formulas as benchmarks. It collects LTL-formulas that have been published in case-studies or tool evaluation papers. We provide the prefix forms of the formula, together with our raw experimentation results and the script plot.R to compile these results into scatter plots download The zip contains three directories: csv, containing the results of our experiments as csv logs, properties, the LTL formulas, and scripts, containing plot.R and stats.R.

The entries in the “tool” column of the csv files map to the configurations given in the paper as follows:

The WDBA-recognizable formulas of each formula set are listed in the directory “obligations”. To produce a scatterplot comparing Duggi with ltl2tgba on the non-wdba-recognizable fragment in “rabinizer3.ltl”, you can invoke plot.R as follows:

 $ scripts/plot.R --standalone -n -f "obligations" -x "./duggi.autfilt.no-wdba.sh" -y "ltl2tgba -U -B --lbt-input -x wdba-minimize=0 -f" data/rabinizer3.csv

The graphics from Figure 13 et seq. can be constructed via scripts/stats.R. You can specify the figure to generate via --generate. For --generate You can specify either a number corresponding to the figure, or the options tab2 (for generating Table 2), tab3 (for generating Table 3), or text for generating the text information. Since most on the information is based on non-WDBA fragment, please additionally specify a file containing the WDBA realizable formulas via -f. In additional_material.tar.gz, this file is properties/ltlstore/obligations.ltl. When generating figures, the tex codes are generated as files, e.g., for --generate 13, the files fig13a.tex, fig13b.tex, fig13c.tex, fig13d.tex are generated. For an ease of use, we provide a --standalone switch, which compiles the tex file into a standalone graphic. Please have latexmk and lualatex installed on your system for this.

Markov chain analysis

You can download a zip with the models, properties and data logs here. Unpack the archive as follows:

$ tar xzf pmc.tar.gz

The structure of the archive is as follows

brp
|- model
|- properties
|- logs
cluster
|- model
|- properties
|- logs

The model of each benchmark of the bounded retransmission protocol (BRP) resp. cluster protocol can be found as brp/model/brp.pm and cluster/model/cluster.sm. The properties are collected in brp/properties/brp.pctl and cluster/properties/cluster.pctl. At last, the logs of our runs can be found the subdirectories */logs/prism-uba.duggi.log and */logs/prism-uba.ltl2tgba.log for the tools duggi and ltl2tgba.

As an example for a commandline we execute

prism-uba/prism/bin/prism -ltluba -pf 'P=?[(s!=4) U (s=3 & s!=4 & (X s!=4)& (X X s=4))]' brp/model/brp.pm -explicit -ltl2datool prism-uba/prism/etc/scripts/hoa/hoa-duggi-uba-for-prism -ltl2dasyntax lbt -const 'N=16,MAX=128' -keepAPs -ubapower -ubareachmethod gs

which executes the BRP benchmark with φ₂^steps. The UBA-based analysis is started with the parameters -ltluba, -ubapower, and -ubareachmethod gs. The explicit engine is activated via -explicit. The -ltl2datool prism-uba/prism/etc/scripts/hoa/hoa-duggi-uba-for-prism switch and the -ltl2dasyntax lbt tells PRISM to execute the script hoa-duggi-uba-for-prism which itself executes duggi. Here, the -ltl2dasyntax lbt tells PRISM to input the LTL formula in the prefix syntax to duggi.

Additionally, we needed to set the flag -keepAPs in the BRP benchmark to forbid PRISM to summarize boolean subformulas to new atomic proposition. This ensures, that s=3 & s!=4 is taken over to p1 & p0 and not summarized to a new atomic proposition p2. Please note, the flag -keepAPs is not used in the cluster benchmark.

At last, the model is set via the positional argument brp/model/brp.pm. The model needs additional constants, which are given by -const 'N=16,MAX=128'.

Alternatively to duggi, you can use ltl2tgba via -ltl2datool prism-uba/prism/etc/scripts/hoa/hoa-spot-uba-for-prism. Please note, that either way, we advice you to edit both scripts manually to set the correct paths in the scripts.

The case study for the cluster benchmark behaves very similar, therefore we just give you the analogous commandline:

prism-uba/prism/bin/prism -ltluba -pf 'P=?[(G F left_n=N) | (F G right_n=N) | (F G right_n=(N-1)) | (F G right_n=(N-2)) | (F G right_n=(N-3)) | (F G right_n=(N-4)) | (F G right_n=(N-5))]' cluster/model/cluster.sm -explicit -ltl2datool prism-uba/prism/etc/scripts/hoa/hoa-duggi-uba-for-prism -ltl2dasyntax lbt -const 'N=16' -pathviaautomata -ubapower -ubareachmethod gs