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.

Following the long standing tradition of naming tools exactly, what they are doing (such as ltl2ba, ltl2dstar, ltl2tgba and ltl2tgta), ltl2dra was picked.

Publications

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

Try it out online!

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).