Making Streett Determinization Tight

Optimal determinization construction of Streett automata is an important research problem because it is indispensable in numerous applications such as decision problems for tree temporal logics, logic games and system synthesis. This paper presents a transformation from nondeterministic Streett automata (NSA) with n states and k Streett pairs to equivalent deterministic Rabin transition automata (DRTA) with n5n(n!)n states, O(nn2) Rabin pairs for k = ω(n) and n5nknk states, O(knk) Rabin pairs for k = O(n). This improves the state of the art Streett determinization construction with n5n(n!)n+1 states, O(n2) Rabin pairs and n5nknkn! states, O(nk) Rabin pairs, respectively. Moreover, deterministic parity transition automata (DPTA) are obtained with 3(n(n + 1) -- 1)!(n!)n+1 states, 2n(n +1) priorities for k = ω(n) and 3(n(k +1) -- 1)!n!knk states, 2n(k + 1) priorities for k = O(n), which improves the best construction with nn(k + 1)n(k+1)(n(k + 1) -- 1)! states, 2n(k + 1) priorities. Further, we prove a lower bound state complexity for determinization construction from N-SA to deterministic Rabin (transition) automata i.e. n5n(n!)n for k = ω(n) and n5nknk for k = O(n), which matches the state complexity of the proposed determinization construction. Besides, we put forward a lower bound state complexity for determinization construction from NSA to deterministic parity (transition) automata i.e. 2ω(n2 log n) for k = ω(n) and 2ω(nk log nk) for k = O(n), which is the same as the state complexity of the proposed determinization construction in the exponent.