A Simple and Optimal Complementation Algorithm for Buchi Automata

Complementation of Buchi automata is complex as Buchi automata in general are nondeterministic. A worst-case state-space growth of O((0.76n)(n)) cannot be avoided. Experiments suggest that complementation algorithms perform better on average when they are structurally simple. We present a simple algorithm for complementing Buchi automata, operating directly on subsets of states, structured into state-set tuples (similar to slices), and producing a deterministic automaton. Then a complementation procedure is applied that resembles the straightforward complementation algorithm for deterministic Buchi automata, the latter algorithm actually being a special case of our construction. Finally, we prove our construction to be optimal, i.e. having an upper bound in O((0.76n)(n)), and furthermore calculate the 0.76 factor in a novel exact way.