Modular Mix-and-Match Complementation of Büchi Automata (Technical Report)

Complementation of nondeterministic Büchi automata (BAs) is animportant problem in automata theory with numerous applications in formal verification, such as termination analysis of programs, model checking, or in decisionprocedures 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 procedurestogether, with one procedure for a subset of the BAs strongly connected components (SCCs). In this way, one can exploit the structure of particular SCCs (suchas when they are inherently weak or deterministic) and use more efficient specialized algorithms, regardless of the structure of the whole BA. We give a generalframework into which partial complementation procedures can be plugged in, andits instantiation with several algorithms. The framework can, in general, produce acomplement with an Emerson-Lei acceptance condition, which can often be morecompact. Using the algorithm, we were able to establish an exponentially betternew upper bound of O(4^n) for complementation of the recently introduced classof elevator automata. We implemented the algorithm in a prototype and performeda comprehensive set of experiments on a large set of benchmarks, showing thatour framework complements well the state of the art and that it can serve as a basisfor future efficient BA complementation and inclusion checking algorithms.