Determinization and limit-determinization of Emerson-Lei automata

DOI10.1007/978-3-030-88885-5_2MaRDI QIDQ2147175zbMATHOpenAlexFDO

Authors Tobias John, Simon Jantsch, Christel Baier, Sascha Klüppelholz

Publication date 22 June 2022

Full work available at URL https://arxiv.org/abs/2106.15892

Mathematics Subject Classification ID

Formal languages and automata (68Q45)

Abstract: We study the problem of determinizing $omega$-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.

Recommendations

• Practical “Paritizing” of Emerson-Lei Automata
• LTL to deterministic Emerson-Lei automata
• Limit-deterministic Büchi automata for linear temporal logic
• Are good-for-games automata good for probabilistic model checking?
• From LTL to Symbolically Represented Deterministic Automata

Cites work

• scientific article; zbMATH DE number 4124989 (Why is no real title available?)
• scientific article; zbMATH DE number 1973991 (Why is no real title available?)
• scientific article; zbMATH DE number 1487477 (Why is no real title available?)
• scientific article; zbMATH DE number 5585443 (Why is no real title available?)
• Alternating finite automata on \(\omega\)-words
• An improved construction of deterministic omega-automaton using derivatives
• Are good-for-games automata good for probabilistic model checking?
• Generic emptiness check for fun and profit
• Good-for-MDPs automata for probabilistic analysis and reinforcement learning
• LTL to deterministic Emerson-Lei automata
• LTL to smaller self-loop alternating automata and back
• Lazy probabilistic model checking without determinisation
• Limit-deterministic Büchi automata for linear temporal logic
• Modalities for model checking: Branching time logic strikes back
• New optimizations and heuristics for determinization of Büchi automata
• On-the-fly emptiness check of transition-based Streett automata
• One theorem to rule them all: a unified translation of LTL into \(\omega \)-automata
• Owl: a library for \(\omega \)-words, automata, and LTL
• Principles of the SPIN model checker. Foreword by Gerard J. Holzmann
• SPIN
• Simulating alternating tree automata by nondeterministic automata: New results and new proofs of the theorems of Rabin, McNaughton and Safra
• The complexity of probabilistic verification
• Tight Bounds for the Determinisation and Complementation of Generalised Büchi Automata

Cited in

(2)

• Practical “Paritizing” of Emerson-Lei Automata
• Symbolic solution of Emerson-Lei games for reactive synthesis

Describes a project that uses

Uses Software

• PRISM
• SPIN
• jSpin
• SPOT
• Owl
• Delag

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)