Article2337455275: Unterschied zwischen den Versionen
Aus International Center for Computational Logic
Johannes Lehmann (Diskussion | Beiträge) (Die Seite wurde neu angelegt: „{{Publikation Erster Autor |ErsterAutorVorname=Joachim |ErsterAutorNachname=Klein |FurtherAuthors=Christel Baier}} {{Article |Journal=Theoretical Computer Science |Number=2 |Pages=182--195 |Title=Experiments with deterministic $ømega$-automata for formulas of linear temporal logic |Volume=363 |Year=2006 }} {{Publikation Details |DOI Name=10.1016/J.TCS.2006.07.022 |Abstract=This paper addresses the problem of generating deterministic ω-auto…“) |
Johannes Lehmann (Diskussion | Beiträge) K (Textersetzung - „Verifikation und formale quantitative Analyse“ durch „Algebraische und logische Grundlagen der Informatik“) |
||
| Zeile 14: | Zeile 14: | ||
|DOI Name=10.1016/J.TCS.2006.07.022 | |DOI Name=10.1016/J.TCS.2006.07.022 | ||
|Abstract=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. | |Abstract=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= | |Forschungsgruppe=Algebraische und logische Grundlagen der Informatik | ||
}} | }} | ||
Aktuelle Version vom 5. März 2025, 15:42 Uhr
Experiments with deterministic $ømega$-automata for formulas of linear temporal logic
Joachim KleinJoachim Klein, Christel BaierChristel Baier
Joachim Klein, Christel Baier
Experiments with deterministic $ømega$-automata for formulas of linear temporal logic
Theoretical Computer Science, 363(2):182--195, 2006
Experiments with deterministic $ømega$-automata for formulas of linear temporal logic
Theoretical Computer Science, 363(2):182--195, 2006
- 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}
}
