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 2^{O(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.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):

• Sources: ltl2dstar-0.5.4.tar.gz (1.1MB)
• Executable (+sources) for Windows: ltl2dstar-0.5.4.zip (3.0MB)

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

Literature

• 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]

Related Work

• 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