A tool constructing deterministic (generalized) Rabin Automata for LTL (Linear Time Logic). The implementation is extracted from the mechanically verified formalisation. The algorithm is compositional, safra-less, and yields small automata. A detailed description can be found in [1]. The tool itself is automatically extracted from the supplementary Isabelle/HOL theories, which are published in the Archive of Formal Proofs [2]. It is closely related to Rabinizer 3, since both tools implement the same algorithm and inspire each other. The only major difference is that LTL_to_DRA is formally verified, while Rabinizer 3 provides more features and has shorter running times.
The latest stable release including the formalisation can be obtained from the Archive of Formal Proofs. A devolpment snapshot of the code with build scripts is located in the develpment branch of the Archive of Formal Proofs. The tool outputs a custom automaton format, which can be translated to the standard HOA format using the following utility: DRA_to_HOA.nightly.zip.
Following the long standing tradition of naming tools exactly, what they are doing (such as ltl2ba
, ltl2dstar
, ltl2tgba
and ltl2tgta
), ltl2dra
was picked.
Javier Esparza, Jan Křetínský, Salomon Sickert
From LTL to deterministic automata - A safraless compositional approach
FMSD (2016): bibtex / view / full version
Salomon Sickert
Linear Temporal Logic
Archive of Formal Proofs (2016): bibtex / view
Salomon Sickert
Converting Linear Temporal Logic to Deterministic (Generalised) Rabin Automata
Archive of Formal Proofs (2015): bibtex / view
You can easily try out the tool here using the following syntax: F,G,X,U,R,&,|,!
. All other strings are interpreted as atomic propositions. The constructed automaton is then translated to HOAF and rendered using autfilt (Spot) and dot (Graphviz).