ltl2dstar

Overview

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.

Documentation

You can find the documentation of the last released version of ltl2dstar here.

Download

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.

Major changes for version 0.5.3:

Download ltl2dstar (v.0.5.3):

Note: For ltl2dstar to translate from LTL formulas, you need an LTL-to-NBA translator. See documentation for pointers to freely available translators.

Try it!

Temporarily offline
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!

Literature

Related Work

If you are interested in ltl2dstar, you might also be interested in these tools:

(c) 2005-2015, Joachim Klein - j.klein@ltl2dstar.de