A Simple and Optimal Complementation Algorithm for Büchi Automata
Joel D. Allred, Ulrich Ultes‐Nitsche · 2018
Complementation of Büchi automata is complex as Büchi 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 Büchi 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 Büchi 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.