Unifying Buchi Complementation Constructions
============================================

Complementation of Buchi 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 {\em 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 {\em odd ranking}, iff all the
runs are rejecting. The second is the {\em slice-based approach} of \kahler and Wilke. This approach
is based on tracking levels of "split trees" -- run trees in which only essential information
about the history of each run is maintained. While the slice-based construction is conceptually
simple, the complementing automata it generates are exponentially larger than those of the recent
rank-based construction of Schewe, and it suffers from the difficulty of symbolically encoding
levels of split trees.

In this work we reformulate the slice-based approach in terms of run \DAGs and preorders over
states. In doing so, we begin to draw parallels between the rank-based and slice-based approaches.
Through deeper analysis of the slice-based approach, we strongly restrict the nondeterminism it
generates. We are then able to employ the slice-based approach to provide a new odd ranking, called
a {\em retrospective ranking}, that is different from the one provided by Kupferman and Vardi.  This
new ranking allows us to construct a deterministic-in-the-limit rank-based automaton with a highly
restricted transition function.  Further, by phrasing the slice-based approach in terms of ranks,
our approach affords a simple symbolic encoding and achieves the tight bound of Schewe's
construction.