From Nondeterministic Buchi and Streett Automata to Deterministic Parity Automata

Determinisation and complementation are foundational notions in computer science. When considering finite automata on finite words nondeterminisation and complementation are one and the same. Given a nondeterministic finite automaton there exists an exponential construction that gives a deterministic automaton for the same language. Inverting the set of accepting states gives us the automaton for the complement language. In the theory of automata on infinite words determinisation and complementation are much more involved. Safra provides determinisation constructions for B"uchi and for Streett automata that result in deterministic Rabin automata. The construction starts with an automaton with $n$ states (and index $k$ for the Streett case) and results in a Rabin automaton with $n^{O(n)}$ states ($(nk)^{O(nk)}$ states and $O(nk)$ index for the Streett case). Here, we reconsider Safra's determinisation constructions. We show how to construct automata with less states, smaller index, and most importantly, parity acceptance condition. Specifically, starting from a nondeterministic B"uchi automaton with $n$ states our construction yields an automaton with $n^{2n+2}$ states (instead of $(2n)^{3n}$), index $2n-1$ (instead of $4n+1$), and a parity automaton (instead of Rabin). Starting from a nondeterministic Streett automaton with $n$ states and index $k$ our construction yields an automaton with $n^{n(k+2)+2}(k+1)^{2n(k+1)}$ states (instead of $2^{3n(k+1)}n^{2n(k+1)+n}(k+1)^{3n(k+1)}$), index $2n(k+1)$ (instead of $4n(k+1)+1$), and a parity automaton (instead of Rabin). For every practical application, the fact that our automaton is parity saves an additional multiplier of $(2n)!$ in the case of B"uchi and $(2n(k+1))!$ in the case of Streett.