Determinization and Limit-Determinization of Emerson-Lei Automata

Tobias JohnTobias John, Simon JantschSimon Jantsch, Christel BaierChristel Baier, Sascha KlüppelholzSascha Klüppelholz

DOI Link

Tobias John, Simon Jantsch, Christel Baier, Sascha Klüppelholz
Determinization and Limit-Determinization of Emerson-Lei Automata
In Hou, Zhe and Ganesh, Vijay, eds., Automated Technology for Verification and Analysis (ATVA), Lecture Notes in Computer Science, 15--31, 2021. Springer International Publishing

Details
Bibtex

KurzfassungAbstract
We study the problem of determinizing -automata whose acceptance condition is defined on the transitions using Boolean formulas, also known as transition-based Emerson-Lei automata (TELA). The standard approach to determinize TELA first constructs an equivalent generalized Büchi automaton (GBA), which is later determinized. We introduce three new ways of translating TELA to GBA. Furthermore, we give a new determinization construction which determinizes several GBA separately and combines them using a product construction. An experimental evaluation shows that the product approach is competitive when compared with state-of-the-art determinization procedures. We also study limit-determinization of TELA and show that this can be done with a single-exponential blow-up, in contrast to the known double-exponential lower-bound for determinization. Finally, one version of the limit-determinization procedure yields good-for-MDP automata which can be used for quantitative probabilistic model checking.
Forschungsgruppe:Research Group: Algebraische und logische Grundlagen der InformatikAlgebraic and Logical Foundations of Computer Science

@inproceedings{JJBK2021,
  author    = {Tobias John and Simon Jantsch and Christel Baier and Sascha
               Kl{\"{u}}ppelholz},
  title     = {Determinization and Limit-Determinization of Emerson-Lei Automata},
  editor    = {Hou and Zhe and Ganesh and Vijay},
  booktitle = {Automated Technology for Verification and Analysis (ATVA)},
  series    = {Lecture Notes in Computer Science},
  publisher = {Springer International Publishing},
  year      = {2021},
  pages     = {15--31},
  doi       = {10.1007/978-3-030-88885-5_2}
}