LTL3TELA is a tool that translates LTL formulae to deterministic or nondeterministic automata. The translation follows in the following steps.
- The formula is translated into an equivalent Self-loop Alternating Automaton (SLAA)
- The SLAA is dealternated into nondeterministic automaton.
- If needed, the nondeterministic automaton is determinized.
The Spot library https://spot.lrde.epita.fr/ has to be installed. Version 2.6 or higher is required for LTL3TELA to compile and work properly.
make should be enough to compile LTL3TELA.
Use ./ltl3tela -f 'formula to translate'.
See ./ltl3tela -h for more information.
The translation of LTL to deterministic and nondeterministic automata was submitted for presentation at the ATVA 2019 conference. Jupyter notebook Evaluation_ATVA19 contains scripts and other data to evaluate the performance compared to the state-of-the-art tools. The impact of the merging was performed on the set of formulae traditionally used to benchmark LTL translators and on 1000 randomly generated formulae.
If you would like to run the notebook by yourself, you need to have the
following tools installed in PATH on your system.
- SPOT v. 2.7.4 with Python bindings
- Pandas Python library v. 20.3+
- Jupyter notebook v. 5.0+
- LTL3TELA v. 2.0.0
- LTL3BA v. 1.1.3
- Owl v. 18.06
With the standard configuration of Spot, LTL3TELA is unable to set more than 32 acceptance
marks, therefore some larger formulae are only translated with Spot and not with standard
LTL3TELA translation (even if it would, in theory, produce smaller automaton). To specify
larger maximum number of acceptance marks, ./configure Spot with --enable-max-accsets=N.