Rabinizer Verified (ltl2dra)

Description

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.

Download

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.

Naming

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

Publications

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