English
Complementation of Büchi automata is well known for being difficult. In the worst case, a state-space growth of (0:76n)n is unavoidable. Recent studies suggest that “simpler” algorithms perform better than more involved ones on practical cases. In this paper, we present a simple “direct” algorithm for complementing Büchi automata. It involves a structured subset construction (using tuples of subsets of states) that produces a deterministic automaton. This construction leads to a complementation procedure that resembles the straightforward complementation algorithm for deterministic Büchi automata, the latter algorithm actually being a special case of our construction.