On Complementing Nondeterministic Buchi Automata
================================================

Several optimal algorithms have been proposed for the complementation
of nondeterministic B\"uchi word automata.  Due to the intricacy of
the problem and the exponential blow-up that complementation involves,
these algorithms have never been used in practice, even though an
effective complementation construction would be of significant
practical value.  Recently, Kupferman and Vardi described a
complementation algorithm that goes through weak alternating automata
and that seems simpler than previous algorithms. We combine their
algorithm with known and new minimization techniques.  Our approach is
based on optimizations of both the intermediate weak alternating
automaton and the final nondeterministic automaton, and involves
techniques of rank and height reductions, as well as direct and fair
simulation.