On the Power of Unambiguity in Büchi Complementation
This provides incremental improvements in automata theory for formal verification and model checking.
The paper tackles the complementation problem for Büchi automata with finite ambiguity by using reduced run DAGs to optimize rank-based and slice-based constructions, improving state complexity from 2^{O(n log n)} to 2^{O(n)} and from O((3n)^n) to O(4^n).
In this work, we exploit the power of \emph{unambiguity} for the complementation problem of Büchi 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üchi automata with a finite degree of ambiguity. As a result, given a Büchi automaton with $n$ states and a finite degree of ambiguity, the number of states in the complementary Büchi automaton constructed by the classical rank-based and slice-based complementation constructions can be improved, respectively, to $2^{O(n)}$ from $2^{O(n\log n)}$ and to $O(4^n)$ from $O((3n)^n)$.