Tags:Benchmarking, Büchi Automaton, Complementation and Optimal Upper Bound

Abstract:

Complementation of Büchi automata is well known for being complex, as Büchi automata in general are nondeterministic. In the worst case, a state-space growth of $O((0.76n)^n)$ cannot be avoided. Experimental results suggest that complementation algorithms perform better on average when they are structurally simple.

In this paper, 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. The second step in the construction is then 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. 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.

A Simple and Optimal Complementation Algorithm for Büchi Automata