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

摘要

In this paper we revisit Safra's determinization constructions for automataon infinite words. We show how to construct deterministic automata with fewerstates and, most importantly, parity acceptance conditions. Determinization isused in numerous applications, such as reasoning about tree automata,satisfiability of CTL*, and realizability and synthesis of logicalspecifications. The upper bounds for all these applications are reduced byusing the smaller deterministic automata produced by our construction. Inaddition, the parity acceptance conditions allows to use more efficientalgorithms (when compared to handling Rabin or Streett acceptance conditions).