Tight Upper Bounds for Streett and Parity Complementation

Abstract

Complementation of finite automata on infinite words is not only a fundamental problem in automata theory, but also serves as a cornerstone for solving numerous decision problems in mathematical logic, model-checking, program analysis and verification. For Streett complementation, a significant gap exists between the current lower bound $2^{Ω(n\lg nk)}$ and upper bound $2^{O(nk\lg nk)}$, where $n$ is the state size, $k$ is the number of Streett pairs, and $k$ can be as large as $2^{n}$. Determining the complexity of Streett complementation has been an open question since the late '80s. In this paper show a complementation construction with upper bound $2^{O(n \lg n+nk \lg k)}$ for $k = O(n)$ and $2^{O(n^{2} \lg n)}$ for $k = ω(n)$, which matches well the lower bound obtained in \cite{CZ11a}. We also obtain a tight upper bound $2^{O(n \lg n)}$ for parity complementation.

Corrected typos. 23 pages, 3 figures. To appear in the 20th Conference on Computer Science Logic (CSL 2011)