Modular Mix-and-Match Complementation of Büchi Automata

Büchi automata, omega regular languages, complementation

Complementation of nondeterministic Büchi automata (BAs) is an important problem
in automata theory with numerous applications in formal verification, such as
termination analysis of programs, model checking, or in decision procedures of
some logics. We build on ideas from a recent work on BA determinization by Li et
al. and propose a new modular algorithm for BA complementation. Our algorithm
allows to combine several BA complementation procedures together, with one
procedure for a subset of the BAs strongly connected components (SCCs). In this
way, one can exploit the structure of particular SCCs (such as when they are
inherently weak or deterministic) and use more efficient specialized algorithms,
regardless of the structure of the whole BA. We give a general framework into
which partial complementation procedures can be plugged in, and its instantiation
with several algorithms. The framework can, in general, produce a complement with
an Emerson-Lei acceptance condition, which can often be more compact. Using the
algorithm, we were able to establish an exponentially better new upper bound of
O(4^n) for complementation of the recently introduced class of elevator automata.
We implemented the algorithm in a prototype and performed a comprehensive set of
experiments on a large set of benchmarks, showing that our framework complements
well the state of the art and that it can serve as a basis for future efficient
BA complementation and inclusion checking algorithms.