„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

DOI Link

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

Details
Bibtex

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}
}