On the Power of Unambiguity in Buchi Complementation

In this work, we exploit the power of emph{unambiguity} for the complementation problem of Buchi automata by utilizing reduced run directed acyclic graphs (DAGs) over infinite words, in which each vertex has at most one predecessor. We then show how to use this type of reduced run DAGs as a emph{unified tool} to optimize emph{both} rank-based and slice-based complementation constructions for Buchi automata with a finite degree of ambiguity. As a result, given a Buchi automaton with $n$ states and a finite degree of ambiguity, the number of states in the complementary Buchi automaton constructed by the classical rank-based and slice-based complementation constructions can be improved, respectively, to $2^{O(n)}$ from $2^{O(nlog n)}$ and to $O(4^n)$ from $O((3n)^n)$.