From Nondeterministic Büchi and Streett Automata to Deterministic Parity Automata

Abstract

In this paper we revisit Safra's determinization constructions for automata on infinite words. We show how to construct deterministic automata with fewer states and, most importantly, parity acceptance conditions. Determinization is used in numerous applications, such as reasoning about tree automata, satisfiability of CTL*, and realizability and synthesis of logical specifications. The upper bounds for all these applications are reduced by using the smaller deterministic automata produced by our construction. In addition, the parity acceptance conditions allows to use more efficient algorithms (when compared to handling Rabin or Streett acceptance conditions).

21 pages. To appear in Logical Methods in Computer Science (LMCS)

Cited by in corpus (19)

• LTL to Deterministic Emerson-Lei Automata
• From LTL and Limit-Deterministic Büchi Automata to Deterministic Parity Automata
• State of Büchi Complementation
• Determinising Parity Automata
• Index appearance record for transforming Rabin automata into parity automata
• Synthesis of Data Word Transducers
• Reactive Safety
• New Optimizations and Heuristics for Determinization of Büchi Automata
• Profile Trees for Büchi Word Automata, with Application to Determinization
• Tight Bounds for Complementing Parity Automata
• Model-checking Quantitative Alternating-time Temporal Logic on One-counter Game Models
• Planning and Synthesis Under Assumptions
• Learn with SAT to Minimize Büchi Automata
• An Objective Improvement Approach to Solving Discounted Payoff Games
• Generalized Planning: Non-Deterministic Abstractions and Trajectory Constraints
• On the size of disjunctive formulas in the $\mu$-calculus
• Equilibria for Games with Combined Qualitative and Quantitative Objectives
• Making Streett Determinization Tight
• Reactive Synthesis: Branching Logics and Parameterized Systems