Tight Upper Bounds for Streett and Parity Complementation

TL;DR

This paper presents tight upper bounds for Streett and parity automata complementation, closing longstanding gaps between known lower and upper bounds, and advancing theoretical understanding in automata theory.

Contribution

It introduces a new complementation construction with bounds matching the lower bounds, resolving a decades-old open problem in automata complexity.

Findings

Upper bound for Streett complementation: $2^{O(n \\lg n+nk \\lg k)}$ for $k=O(n)$

Upper bound for Streett complementation: $2^{O(n^{2} \\lg n)}$ for $k=\\omega(n)$

Tight upper bound for parity complementation: $2^{O(n \\lg n)}$

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^{\Omega(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 = \omega(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.