Determinization and limit-determinization of Emerson-Lei automata
From MaRDI portal
Publication:2147175
DOI10.1007/978-3-030-88885-5_2zbMATH Open1497.68270arXiv2106.15892OpenAlexW3208208968MaRDI QIDQ2147175FDOQ2147175
Christel Baier, Sascha Klüppelholz, Tobias John, Simon Jantsch
Publication date: 22 June 2022
Abstract: 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"uchi 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.
Full work available at URL: https://arxiv.org/abs/2106.15892
Cites Work
- SPIN
- The complexity of probabilistic verification
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Alternating finite automata on \(\omega\)-words
- Title not available (Why is that?)
- Title not available (Why is that?)
- Modalities for model checking: Branching time logic strikes back
- Simulating alternating tree automata by nondeterministic automata: New results and new proofs of the theorems of Rabin, McNaughton and Safra
- Owl: a library for \(\omega \)-words, automata, and LTL
- Tight Bounds for the Determinisation and Complementation of Generalised Büchi Automata
- Limit-Deterministic Büchi Automata for Linear Temporal Logic
- Lazy probabilistic model checking without determinisation
- One Theorem to Rule Them All
- LTL to smaller self-loop alternating automata and back
- An Improved Construction of Deterministic Omega-automaton Using Derivatives
- New Optimizations and Heuristics for Determinization of Büchi Automata
- Generic Emptiness Check for Fun and Profit
- Title not available (Why is that?)
- On-the-fly Emptiness Check of Transition-Based Streett Automata
- Good-for-MDPs Automata for Probabilistic Analysis and Reinforcement Learning
- Are Good-for-Games Automata Good for Probabilistic Model Checking?
Cited In (2)
Uses Software
This page was built for publication: Determinization and limit-determinization of Emerson-Lei automata
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2147175)
