On the power of finite ambiguity in B?chi complementation

In this work, we exploit the power of finite ambiguity for the complementation problem of Buchi 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 Buchi 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 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 from 2O(n log n) and O((3n)n) to O(6n) c 2O(n) and O(4n), respectively. We further show how to construct such reduced run DAGs for limit deterministic Buchi automata and obtain a specialized complementation algorithm, thus demonstrating the generality of the power of finite ambiguity.(c) 2023 Elsevier Inc. All rights reserved.