On the Power of Unambiguity in Büchi Complementation

Abstract

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)$.

arXiv commentIn Proceedings GandALF 2020, arXiv:2009.09360

References in corpus (6)

• Antichains for the Automata-Based Approach to Model-Checking
• Efficient reduction of nondeterministic automata with application to language inclusion testing
• State of Büchi Complementation
• Lower Bounds for Complementation of omega-Automata Via the Full Automata Technique
• Büchi Complementation and Size-Change Termination
• On finitely ambiguous Büchi automata

Cited by in corpus (1)

• Sky Is Not the Limit: Tighter Rank Bounds for Elevator Automata in Büchi Automata Complementation (Technical Report)