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
Theoretical Computer Science, 363(2):182--195, 2006

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

@article{KB2006,
  author  = {Joachim Klein and Christel Baier},
  title   = {Experiments with deterministic ${\o}mega$-automata for formulas of
             linear temporal logic},
  journal = {Theoretical Computer Science},
  volume  = {363},
  number  = {2},
  year    = {2006},
  pages   = {182--195},
  doi     = {10.1016/J.TCS.2006.07.022}
}