ltl2dstar ("LTL to deterministic Streett and Rabin automata") is a program that converts formulas in Linear Time Logic to deterministic ω-automata, specifically Rabin (DRA) and Streett automata (DSA).
It is an implementation of Safra's construction to translate nondeterministic Büchi automata (NBA) to deterministic Rabin automata, which has a worst-case complexity of 2O(n log n), with n being the number of states in the NBA. ltl2dstar employs optimizations and heuristics in an attempt to generate smaller automata in practice. It uses external LTL-to-Büchi translators for the conversion from LTL to NBA and can thus benefit from the state-of-the-art algorithms, implementations and optimizations available in this well researched area.
You can find the documentation of the last released version of ltl2dstar here.
ltl2dstar is released under the terms of the GNU General Public License version 2.
Refer to NEWS for a description of the changes between versions.
Download ltl2dstar (v.0.5.1):
Note: For ltl2dstar to be functional, you need an LTL-to-NBA translator. See documentation for pointers to freely available translators.
Compilation for GCC versions >=4.4.0:
Starting with GCC version 4.4.0, the version of the Boost C++ library version included in the ltl2dstar-0.5.1 release has problems compiling. You can compile ltl2dstar with these compilers by replacing the src/boost directory in the ltl2dstar source code with the boost/ subdirectory from a current version of Boost, available here.
Scott C. Livingston kindly provides a web interface to ltl2dstar at http://www.cds.caltech.edu/~slivings/sandbox/wrapltl.php, where you can generate deterministic automata for LTL formulas, including visualization. Thanks!
(c) 2005-2013, Joachim Klein - firstname.lastname@example.org