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.
Major changes for version 0.5.4:
- Fixes some non-deterministic parsing errors when reading HOA automata.
- Optimization: Remove irrelevant states during preprocessing of NBA
- Optimization: If the NBA is already deterministic, skip determinization construction but perform stuttering and bisimulation.
- New option --extra-output, allowing to obtain outputs in different formats from the same constructed automaton
Major changes for version 0.5.3:
- More flexible --ltl2nba translator specification, can read HOA NBA
- --input=nba option for determinizing directly from HOA NBA
- Parsing of HOA NBA via cpphoafparser 0.99.1 library
- Compilation now requires C++11 compiler
- Support for parsing Promela neverclaims generated by Spin 6.2.4 and later
Download ltl2dstar (v.0.5.4):
Note: For ltl2dstar to translate from LTL formulas,
you need an LTL-to-NBA translator. See documentation for pointers to
freely available translators.
- Joachim Klein, Christel Baier:
"On-the-fly Stuttering in the Construction of Deterministic omega-Automata"
in: CIAA 2007, Lecture Notes in Computer Science volume 4783, 2007, p51-61
[link]
- Joachim Klein, Christel Baier:
"Experiments with deterministic omega-automata for formulas of linear temporal logic"
in: Theoretical Computer Science, 363/2, 2006, p182-195
[link]
- Joachim Klein:
"Linear Time Logic and Deterministic omega-Automata"
Diploma thesis, January 2005, University of Bonn
[pdf].
- Shmuel Safra:
"On the Complexity of omega-Automata"
FOCS, 1988
[link]
If you are interested in ltl2dstar, you
might also be interested in these tools:
-
Rabinizer 3
and
Rabinizer 4: Java-based translators
from LTL to deterministic Rabin automata and deterministic
generalized Rabin automata, avoiding Safra's construction.
-
ltl3dra: Translator
for a fragment of LTL to
deterministic transition-based generalized Rabin automata,
avoiding Safra's construction.
-
Spot: Different tools related to
manipulating LTL formulas and omega-automata. Supports reading
deterministic Rabin and Streett automata, such as ltlcross.
-
PRISM: Probabilistic model
checker, relies on a Java reimplementation of ltl2dstar for
generating deterministic Rabin automata.
-
cpphoafparser
and jhoafparser:
C++ and Java-based libraries for parsing automata in HOA format.
(C) 2005-2019, Joachim Klein - j.klein@ltl2dstar.de