Overview

LTL3TELA is a tool that translates LTL formulae to deterministic or nondeterministic automata. The translation follows in the following steps.

1. The formula is translated into an equivalent Self-loop Alternating Automaton (SLAA)
2. The SLAA is dealternated into nondeterministic automaton.
3. If needed, the nondeterministic automaton is determinized.

Requirements

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.

Installation

make should be enough to compile LTL3TELA.

Usage

Use ./ltl3tela -f 'formula to translate'. See ./ltl3tela -h for more information.

Experimental evaluation

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.

Requirements

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

Known bugs

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.