Unifying Büchi Complementation Constructions

Seth Fogarty, Orna Kupferman, Moshe Y. Vardi & Thomas Wilke
Complementation of Buechi automata, required for checking automata containment, is of major theoretical and practical interest in formal verification. We consider two recent approaches to complementation. The first is the rank-based approach of Kupferman and Vardi, which operates over a DAG that embodies all runs of the automaton. This approach is based on the observation that the vertices of this DAG can be ranked in a certain way, termed an odd ranking, iff all runs...