On minimal odd rankings for Büchi complementation

Abstract

We study minimal odd rankings (as defined by Kupferman and Vardi[KV01]) for run-DAGs of words in the complement of a nondeterministic Büchi automaton. We present an optimized version of the ranking based complementation construction of Friedgut, Kupferman and Vardi[FKV06] and Schewe's[Sch09] variant of it, such that every accepting run of the complement automaton assigns a minimal odd ranking to the corresponding run-DAG. This allows us to determine minimally inessential ranks and redundant slices in ranking-based complementation constructions. We exploit this to reduce the size of the complement Büchi automaton by eliminating all redundant slices. We demonstrate the practical importance of this result through a set of experiments using the NuSMV model checker. © 2009 Springer-Verlag Berlin Heidelberg.