LTL to Deterministic Emerson-Lei Automata

David MüllerDavid Müller, Salomon SickertSalomon Sickert

DOI Link

David Müller, Salomon Sickert
LTL to Deterministic Emerson-Lei Automata
Proc. of the 8th International Symposium on Games, Automata, Logics and Formal Verification (GandALF), volume 256 of Electronic Proceedings in Theoretical Computer Science, 180--194, 2017. Open Publishing Association

Details
Bibtex

KurzfassungAbstract
We introduce a new translation from linear temporal logic (LTL) to deterministic Emerson-Lei automata, which are omega-automata with a Muller acceptance condition symbolically expressed as a Boolean formula. The richer acceptance condition structure allows the shift of complexity from the state space to the acceptance condition. Conceptually the construction is an enhanced product construction that exploits knowledge of its components to reduce the number of states. We identify two fragments of LTL, for which one can easily construct deterministic automata and show how knowledge of these components can reduce the number of states. We extend this idea to a general LTL framework, where we can use arbitrary LTL to deterministic automata translators for parts of formulas outside the mentioned fragments. Further, we show succinctness of the translation compared to existing construction. The construction is implemented in the tool Delag, which we evaluate on several benchmarks of LTL formulas and probabilistic model checking case studies.
Forschungsgruppe:Research Group: Algebraische und logische Grundlagen der InformatikAlgebraic and Logical Foundations of Computer Science

@inproceedings{MS2017,
  author    = {David M{\"{u}}ller and Salomon Sickert},
  title     = {LTL to Deterministic Emerson-Lei Automata},
  booktitle = {Proc. of the 8th International Symposium on Games, Automata,
               Logics and Formal Verification (GandALF)},
  series    = {Electronic Proceedings in Theoretical Computer Science},
  volume    = {256},
  publisher = {Open Publishing Association},
  year      = {2017},
  pages     = {180--194},
  doi       = {10.4204/EPTCS.256.13}
}