有限模糊性在Büchi补全中的能量
摘要：利用有限歧义的力量来解决Buchi自动机的补问题：使用指向无限词的降低运行有向无环图（DAGs），其中每个顶点最多只有一个前驱；这些降低运行DAGs仅有有限数量的无限运行，从而获得Buchi补充问题中的有限歧义。我们展示了如何将这种类型的降低运行DAGs作为优化基于等级和基于切片补充构造的统一工具，用于具有有限歧义的Buchi自动机。结果是，对于给定具有n个状态和有限歧义度的Buchi自动机，由经典的基于等级和基于切片补充构造构建的互补Buchi自动机的状态数可以从O(n log n)和O((3n)^n)改进为O(6^n)⊆2^{O(n)}和O(4^n)。我们进一步展示了如何为极限确定性Buchi自动机构造这种降低运行DAGs并获得专门的补充算法，从而展示了有限歧义的力量的普适性。
作者：Weizhi Feng, Yong Li, Andrea Turrini, Moshe Y. Vardi, Lijun Zhang
论文ID：2109.12828
分类：Formal Languages and Automata Theory
分类简称：cs.FL
提交时间：2023-03-06