×

From nondeterministic Büchi and Streett automata to deterministic parity automata. (English) Zbl 1125.68067

Summary: 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 allow us to use more efficient algorithms (when compared to handling Rabin or Streett acceptance conditions).

MSC:

68Q45 Formal languages and automata
03D05 Automata and formal grammars in connection with logical questions
68Q60 Specification and verification (program logics, model checking, etc.)
Full Text: DOI