From Emerson-Lei Automata to Deterministic, Limit-Deterministic or Good-for-MDP Automata
From International Center for Computational Logic
From Emerson-Lei Automata to Deterministic, Limit-Deterministic or Good-for-MDP Automata
Tobias JohnTobias John, Simon JantschSimon Jantsch, Christel BaierChristel Baier, Sascha KlüppelholzSascha Klüppelholz
Tobias John, Simon Jantsch, Christel Baier, Sascha Klüppelholz
From Emerson-Lei Automata to Deterministic, Limit-Deterministic or Good-for-MDP Automata
Innovations in Systems and Software Engineering, 2022
From Emerson-Lei Automata to Deterministic, Limit-Deterministic or Good-for-MDP Automata
Innovations in Systems and Software Engineering, 2022
- KurzfassungAbstract
The topic of this paper is the determinization problem of ω-automata under the transition-based Emerson-Lei acceptance (called TELA), which generalizes all standard acceptance conditions and is defined using positive Boolean formulas. Such automata can be determinized by first constructing an equivalent generalized Büchi automaton (GBA), which is later determinized. The problem of constructing an equivalent GBA is considered in detail, and three new approaches of solving it are proposed. Furthermore, a new determinization construction is introduced 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. The second part of the paper studies limit-determinization of TELA and we 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
@article{JJBK2022,
author = {Tobias John and Simon Jantsch and Christel Baier and Sascha
Kl{\"{u}}ppelholz},
title = {From Emerson-Lei Automata to Deterministic, Limit-Deterministic or
Good-for-MDP Automata},
journal = {Innovations in Systems and Software Engineering},
year = {2022},
doi = {10.1007/s11334-022-00445-7}
}