On the Power of Finite Ambiguity in B\"uchi Complementation

TL;DR

This paper introduces a novel approach leveraging finite ambiguity in B"uchi automata to optimize complementation constructions, significantly reducing the state complexity of the resulting automata.

Contribution

It develops a unified framework using reduced run DAGs to improve classical rank-based and slice-based B"uchi complementation methods for finitely ambiguous automata.

Findings

State complexity improved from exponential to subexponential bounds.

Unified approach applies to both rank-based and slice-based methods.

Extension to limit deterministic B"uchi automata demonstrates versatility.

Abstract

In this work, we exploit the power of \emph{finite ambiguity} for the complementation problem of B\"uchi automata by using reduced run directed acyclic graphs (DAGs) over infinite words, in which each vertex has at most one predecessor; these reduced run DAGs have only a finite number of infinite runs, thus obtaining the finite ambiguity in B\"uchi complementation. We show how to use this type of reduced run DAGs as a unified tool to optimize 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 $n$ 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 from $2^{\mathsf{O}(n \log n)}$ and $\mathsf{O}((3n)^{n})$ to $\mathsf{O}(6^{n}) \subseteq 2^{\mathsf{O}(n)}$ and $\mathsf{O}(4^{n})$, respectively. We further show how to construct such reduced run DAGs for limit deterministic B\"uchi automata and obtain a specialized complementation algorithm, thus demonstrating the generality of the power of finite ambiguity.