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²ⁿ⁺² states and index 2n (instead of a Rabin automaton with (12)ⁿn²ⁿ 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²n!(or(n(k+1))²(n(k+1))! in the case of Streett) which is saved using our construction