Complementing Büchi automata with a subset-tuple construction
Joel D. Allred, Ulrich Ultes‐Nitsche · 2015
Complementation of Buchi automata is well known for being difficult. In the worst case, a state-space growth of (0.76n) 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 Buchi 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 Buchi automata, the latter algorithm actually being a special case of our construction.