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. © Springer-Verlag Berlin Heidelberg 2006.
CITATION STYLE
Klein, J. chim, & Baier, C. (2006). Experiments with deterministic ω-automata for formulas of linear temporal logic. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 3845 LNCS, pp. 199–212). https://doi.org/10.1007/11605157_17
Mendeley helps you to discover research relevant for your work.