论有限歧义性在 Büchi 自动机补运算中的威力
形式语言与自动机理论
2023-03-06 v2
摘要
在这项工作中，我们利用有限歧义性的威力来解决 Büchi 自动机的补问题，方法是在无限字上使用归约运行有向无环图（DAG），其中每个顶点最多有一个前驱；这些归约运行 DAG 只有有限数量的无限运行，从而在 Büchi 补运算中获得了有限歧义性。我们展示了如何将这种类型的归约运行 DAG 作为统一工具，来优化具有有限歧义度的 Büchi 自动机的基于秩和基于切片的补构造。结果表明，给定一个具有 n 个状态和有限歧义度的 Büchi 自动机，由经典的基于秩和基于切片的补构造所构建的补 Büchi 自动机的状态数可以分别从 2^{O(n log n)} 和 O((3n)^{n}) 改进到 O(6^{n}) ⊆ 2^{O(n)} 和 O(4^{n})。我们进一步展示了如何为极限确定型 Büchi 自动机构造此类归约运行 DAG，并获得一个专用的补算法，从而证明了有限歧义性威力的普适性。
引用
@article{arxiv.2109.12828,
title = {On the Power of Finite Ambiguity in B\"uchi Complementation},
author = {Weizhi Feng and Yong Li and Andrea Turrini and Moshe Y. Vardi and Lijun Zhang},
journal= {arXiv preprint arXiv:2109.12828},
year = {2023}
}