Additional material to the GandALF paper "LTL to Deterministic Emerson-Lei Automata"

Additional material to the GandALF paper "LTL to Deterministic Emerson-Lei Automata"

On this home page you find the implementation of Delag and PRISM to reproduce the experiments of the paper.

Delag

You can find a zip of Delag here. Please note the README file in the top directory (and ignore the README.md file). Shortly, 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

File Description
literature.ltl Literature formulas of [29,7,10]
alternating.ltl Formula phi_{R,n} for n from 0 to 8
historyVsAfter.ltl Formula phi_{H,n} for n from 0 to 10

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 (wlan2.pm) and the properties (wlanX.pctl). Please note, since we reused some properties for maximal and minimal probabilities, the mapping is as follows:

File Description
wlan1.pctl Pmin(varphi1)
wlan2.pctl Pmin(varphi2)
wlan3.pctl Pmin(varphi3)
wlan4.pctl Pmin(varphi4)
wlan5.pctl Pmax(varphi4)
wlan6.pctl Pmin(varphi5)
wlan7.pctl Pmax(varphi5)
wlan8.pctl Pmin(varphi6)
wlan9.pctl Pmin(varphi7)

SPOT

We use SPOT (version 2.3.8) for some LTL formula format translations. To install SPOT, please follow the instructions here. We configured and compiled SPOT with the options --disable-devel and --disable-debug.