论无歧义性在 Büchi 补集构造中的威力

在这项工作中，我们利用基于无限字上的约简运行有向无环图（DAG）来发掘\emph{无歧义性}在 Büchi 自动机补集问题中的威力，其中每个顶点至多有一个前驱。然后我们展示如何使用这类约简运行 DAG 作为一种\emph{统一工具}，以优化具有有限歧义度的 Büchi 自动机的基于秩和基于切片的两类补集构造。结果表明，给定一个具有 $n$ 个状态和有限歧义度的 Büchi 自动机，由经典基于秩和基于切片的补集构造所构造的补 Büchi 自动机的状态数可分别从 $2^{O(n\log n)}$ 和 $O((3n)^n)$ 改进到 $2^{O(n)}$ 和 $O(4^n)$。