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 . The tool itself is automatically extracted from the supplementary Isabelle/HOL theories, which are published in the Archive of Formal Proofs . 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 exaclty, what they are doing (such as
ltl2dra was picked.
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).