Making Streett Determinization Tight

TL;DR

This paper introduces a new, more efficient method for converting nondeterministic Streett automata into deterministic Rabin and parity automata, with proven optimality in state complexity.

Contribution

It presents a tight determinization construction for Streett automata, improving existing bounds and matching lower bounds for state complexity.

Findings

New determinization construction with improved state bounds

Matching lower bounds for state complexity

Enhanced automata transformation techniques

Abstract

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 $n^{5n}(n!)^{n}$ states, $O(n^{n^2})$ Rabin pairs for $k=\omega(n)$ and $n^{5n}k^{nk}$ states, $O(k^{nk})$ Rabin pairs for $k=O(n)$. This improves the state of the art Streett determinization construction with $n^{5n}(n!)^{n+1}$ states, $O(n^2)$ Rabin pairs and $n^{5n}k^{nk}n!$ 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=\omega(n)$ and $3(n(k+1)-1)!n!k^{nk}$ states, $2n(k+1)$ priorities for $k=O(n)$, which improves the best construction with $n^{n}(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 NSA to deterministic Rabin (transition) automata i.e. $n^{5n}(n!)^{n}$ for $k=\omega(n)$ and $n^{5n}k^{nk}$ 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^{\Omega(n^2 \log n)}$ for $k=\omega(n)$ and $2^{\Omega(nk \log nk)}$ for $k=O(n)$, which is the same as the state complexity of the proposed determinization construction in the exponent.