From nondeterministic Buchi and Streett automata to deterministic parity automata

In this paper we revisit Safra's determinization constructions. We show how to construct deterministic automata with fewer states and, most importantly, parity acceptance conditions. Specifically, starting from a nondeterministic Buchi automaton with n states our construction yields a deterministic parity automaton with n(2n+2) states and index 2n (instead of a Rabin automaton with (12)(n)n(2n) states and n pairs). Starting from a nondeterministic Streett automaton with n states and k pairs our construction yields a deterministic parity automaton with n(n(k+2)+2) (k+ 1)(2n(k+1)) states and index 2n(k + 1) (instead of a Rabin automaton with (12)(n(k+1))n(n(k+2)) (k+ 1)(2n)(k+1) states and n(k + 1) pairs). The parity condition is much simpler than the Rabin condition. In applications such as solving games and emptiness of tree automata handling the Rabin condition involves an additional multiplier of n(2)n! (or (n(k + 1))(2) (n (k + 1))! in the case of Streett) which is saved using our construction.