Article2095125191: Unterschied zwischen den Versionen
Aus International Center for Computational Logic
Johannes Lehmann (Diskussion | Beiträge) (Die Seite wurde neu angelegt: „{{Publikation Erster Autor |ErsterAutorVorname= Simon |ErsterAutorNachname=Jantsch |FurtherAuthors= David Müller; Christel Baier; Joachim Klein}} {{Article |Journal=Formal Methods in System Design |Month=December |Title=From LTL to Unambiguous Büchi Automata via Disambiguation of Alternating Automata |Year=2021 }} {{Publikation Details |DOI Name=10.1007/s10703-021-00379-z |Abstract=Due to the high complexity of translating linear temporal…“) |
Johannes Lehmann (Diskussion | Beiträge) K (Textersetzung - „Verifikation und formale quantitative Analyse“ durch „Algebraische und logische Grundlagen der Informatik“) |
||
| Zeile 12: | Zeile 12: | ||
|DOI Name=10.1007/s10703-021-00379-z | |DOI Name=10.1007/s10703-021-00379-z | ||
|Abstract=Due to the high complexity of translating linear temporal logic (LTL) to deterministic automata, several forms of “restricted” nondeterminism have been considered with the aim of maintaining some of the benefits of deterministic automata, while at the same time allowing more efficient translations from LTL. One of them is the notion of unambiguity. This paper proposes a new algorithm for the generation of unambiguous Büchi automata (UBA) from LTL formulas. Unlike other approaches it is based on a known translation from very weak alternating automata (VWAA) to NBA. A notion of unambiguity for alternating automata is introduced and it is shown that the VWAA-to-NBA translation preserves unambiguity. Checking unambiguity of VWAA is determined to be PSPACE-complete, both for the explicit and symbolic encodings of alternating automata. The core of the LTL-to-UBA translation is an iterative disambiguation procedure for VWAA. Several heuristics are introduced for different stages of the procedure. We report on an implementation of our approach in the tool Duggi and compare it to an existing LTL-to-UBA implementation in the SPOT tool set. Our experiments cover model checking of Markov chains, which is an important application of UBA. | |Abstract=Due to the high complexity of translating linear temporal logic (LTL) to deterministic automata, several forms of “restricted” nondeterminism have been considered with the aim of maintaining some of the benefits of deterministic automata, while at the same time allowing more efficient translations from LTL. One of them is the notion of unambiguity. This paper proposes a new algorithm for the generation of unambiguous Büchi automata (UBA) from LTL formulas. Unlike other approaches it is based on a known translation from very weak alternating automata (VWAA) to NBA. A notion of unambiguity for alternating automata is introduced and it is shown that the VWAA-to-NBA translation preserves unambiguity. Checking unambiguity of VWAA is determined to be PSPACE-complete, both for the explicit and symbolic encodings of alternating automata. The core of the LTL-to-UBA translation is an iterative disambiguation procedure for VWAA. Several heuristics are introduced for different stages of the procedure. We report on an implementation of our approach in the tool Duggi and compare it to an existing LTL-to-UBA implementation in the SPOT tool set. Our experiments cover model checking of Markov chains, which is an important application of UBA. | ||
|Forschungsgruppe= | |Forschungsgruppe=Algebraische und logische Grundlagen der Informatik | ||
}} | }} | ||
Aktuelle Version vom 5. März 2025, 15:45 Uhr
„December“ befindet sich nicht in der Liste (Januar, Februar, März, April, Mai, Juni, Juli, August, September, Oktober, ...) zulässiger Werte für das Attribut „Month“.
From LTL to Unambiguous Büchi Automata via Disambiguation of Alternating Automata
Simon JantschSimon Jantsch, David MüllerDavid Müller, Christel BaierChristel Baier, Joachim KleinJoachim Klein
Simon Jantsch, David Müller, Christel Baier, Joachim Klein
From LTL to Unambiguous Büchi Automata via Disambiguation of Alternating Automata
Formal Methods in System Design, 2021
From LTL to Unambiguous Büchi Automata via Disambiguation of Alternating Automata
Formal Methods in System Design, 2021
- KurzfassungAbstract
Due to the high complexity of translating linear temporal logic (LTL) to deterministic automata, several forms of “restricted” nondeterminism have been considered with the aim of maintaining some of the benefits of deterministic automata, while at the same time allowing more efficient translations from LTL. One of them is the notion of unambiguity. This paper proposes a new algorithm for the generation of unambiguous Büchi automata (UBA) from LTL formulas. Unlike other approaches it is based on a known translation from very weak alternating automata (VWAA) to NBA. A notion of unambiguity for alternating automata is introduced and it is shown that the VWAA-to-NBA translation preserves unambiguity. Checking unambiguity of VWAA is determined to be PSPACE-complete, both for the explicit and symbolic encodings of alternating automata. The core of the LTL-to-UBA translation is an iterative disambiguation procedure for VWAA. Several heuristics are introduced for different stages of the procedure. We report on an implementation of our approach in the tool Duggi and compare it to an existing LTL-to-UBA implementation in the SPOT tool set. Our experiments cover model checking of Markov chains, which is an important application of UBA. - Forschungsgruppe:Research Group: Algebraische und logische Grundlagen der InformatikAlgebraic and Logical Foundations of Computer Science
@article{JMBK2021,
author = {Simon Jantsch and David M{\"{u}}ller and Christel Baier and Joachim
Klein},
title = {From {LTL} to Unambiguous B{\"{u}}chi Automata via Disambiguation
of Alternating Automata},
journal = {Formal Methods in System Design},
year = {2021},
doi = {10.1007/s10703-021-00379-z}
}
