Yong Li (State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences) |
Moshe Y. Vardi (Rice University) |
Lijun Zhang (State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences) |
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 2^O(n) from 2^O(nlogn) and to O(4^n) from O((3n)^n). |
ArXived at: https://dx.doi.org/10.4204/EPTCS.326.12 | bibtex | |
Comments and questions to: eptcs@eptcs.org |
For website issues: webmaster@eptcs.org |