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
Proc. of the 23rd International Symposium on Formal Methods (FM), Lecture Notes in Computer Science, 262--279, 2019. Springer

Details
Bibtex

KurzfassungAbstract
This paper proposes a new algorithm for the generation of unambiguous Büchi automata (UBA) from LTL formulas. Unlike existing tableau-based LTL-to-UBA translations, our algorithm deals with very weak alternating automata (VWAA) as an intermediate representation. It relies on a new notion of unambiguity for VWAA and a disambiguation procedure for VWAA. We introduce optimizations on the VWAA level and new LTL simplifications targeted at generating small UBA. We report on an implementation of the construction in our tool Duggi and discuss experimental results that compare the automata sizes and computation times of Duggi with the tableau-based LTL-to-UBA translation of the SPOT tool set. Our experiments also cover the analysis of Markov chains under LTL specifications, which is an important application of UBA.
Forschungsgruppe:Research Group: Algebraische und logische Grundlagen der InformatikAlgebraic and Logical Foundations of Computer Science

The final publication is available at Springer via http://dx.doi.org/10.1007/978-3-030-30942-8_17.

@inproceedings{JMBK2019,
  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},
  booktitle = {Proc. of the 23rd International Symposium on Formal Methods (FM)},
  series    = {Lecture Notes in Computer Science},
  publisher = {Springer},
  year      = {2019},
  pages     = {262--279},
  doi       = {10.1007/978-3-030-30942-8_17}
}