Experiments with Deterministic $ømega$-Automata for Formulas of Linear temporal Logic

Joachim KleinJoachim Klein, Christel BaierChristel Baier

DOI Link

Joachim Klein, Christel Baier
Experiments with Deterministic $ømega$-Automata for Formulas of Linear temporal Logic
Proc. of the 10th International Conference on Implementation and Application of Automata (CIAA), volume 3845 of Lecture Notes in Computer Science, 199--212, 2005. Springer

Details
Bibtex

KurzfassungAbstract
This paper addresses the problem of generating deterministic ω-automata for formulas of linear temporal logic, which can be solved by applying well-known algorithms to construct a nondeterministic Büchi automaton for the given formula on which we then apply a determinization algorithm. We study here in detail Safra's determinization algorithm, present several heuristics that attempt to decrease the size of the resulting automata and report on experimental results.
Forschungsgruppe:Research Group: Algebraische und logische Grundlagen der InformatikAlgebraic and Logical Foundations of Computer Science

The final publication is available at Springer via http://dx.doi.org/10.1007/11605157_17.

@inproceedings{KB2005,
  author    = {Joachim Klein and Christel Baier},
  title     = {Experiments with Deterministic ${\o}mega$-Automata for Formulas
               of Linear temporal Logic},
  booktitle = {Proc. of the 10th International Conference on Implementation and
               Application of Automata (CIAA)},
  series    = {Lecture Notes in Computer Science},
  volume    = {3845},
  publisher = {Springer},
  year      = {2005},
  pages     = {199--212},
  doi       = {10.1007/11605157_17}
}