2020/05/31 by Yong Li, Moshe Y. Vardi, Lijun Zhang
Computer Science · #cs.FL #cs.CL
paper · pdf · doi:10.4204/eptcs.326.12
published as EPTCS 326, 2020, pp. 182-198 · In Proceedings GandALF 2020, arXiv:2009.09360
arxiv created 2020/09/23 · arxiv updated 2020/09/24
In this work, we exploit the power of 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 unified tool to optimize 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 2O(n) from 2O(nlog n) and to O(4n) from O((3n)n).