In this work, we exploit the power of \emph{unambiguity} for the complementation problem of B"uchi 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 B"uchi automata with a finite degree of ambiguity. As a result, given a B"uchi automaton with states and a finite degree of ambiguity, the number of states in the complementary B"uchi automaton constructed by the classical rank-based and slice-based complementation constructions can be improved, respectively, to from and to from .

生成讲解博客的中文版本

生成AI智能校验的中文版本