From Nondeterministic Buchi and Streett Automata to Deterministic Parity Automata

Determinization and complementation are fundamental notions in computer science. When considering finite automata on finite words determinization gives also a solution to complementation. Given a nondeterministic finite automaton there exists an exponential construction that gives a deterministic automaton for the same language. Dualizing the set of accepting states gives an automaton for the complement language. In the theory of automata on infinite words, determinization and complementation are much more involved. Safra provides determinization constructions for Buchi and Streett automata that result in deterministic Rabin automata. For a Buchi automaton with n states, Safra constructs a deterministic Rabin automaton with nO(n) states and n pairs. For a Streett automaton with n states and k pairs, Safra constructs a deterministic Rabin automaton with (nk)O(nk) states and n(k+1) pairs.

Here, we reconsider Safra's determinization constructions. We show how to construct automata with fewer states and, most importantly, parity acceptance condition. Specifically, starting from a nondeterministic B\"uchi automaton with n states our construction yields a deterministic parity automaton with n2n+2 states and index 2n (instead of a Rabin automaton with (12)nn2n states and n pairs). Starting from a nondeterministic Streett automaton with n states and k pairs our construction yields a deterministic parity automaton with nn(k+2)+2(k+1)2n(k+1) states and index 2n(k+1) (instead of a Rabin automaton with (12)n(k+1)nn(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 n2n! (or (n(k+1))2(n(k+1))! in the case of Streett) which is saved using our construction.


PDF