Büchi Complementation Made Tight

Sven Schewe
The precise complexity of complementing B\"uchi\ automata is an intriguing and long standing problem. While optimal complementation techniques for finite automata are simple -- it suffices to determinize them using a simple subset construction and to dualize the acceptance condition of the resulting automaton -- B\"uchi\ complementation is more involved. Indeed, the construction of an EXPTIME complementation procedure took a quarter of a century from the introduction of B\"uchi\ automata in the early $60$s, and...