非确定性和概率布尔谢自动机的公平模拟：一个共代数视角
摘要：关于模拟的概念，除了其他应用之外，为语言包含提供了一个可计算且有效（但不一定完整）的证明方法。Lynch和Vaandrager对非确定性和时态系统进行了全面的研究；对于B"{u}chi自动机，Henzinger，Kupferman和Rajamani引入了公平模拟的概念。我们在两个不同的方向上对公平模拟进行了推广研究：一种是之前由Bomhard研究过的非确定性树自动机；另一种是带有有限状态空间的概率词自动机，两者都遵循B"{u}chi接受条件。前者的非确定性定义是以固定点方程系统的形式表述的，因此很容易转化为平衡博弈，并且适用于Jurdzi''{n}ski的算法；后者的概率定义具有很强的排名函数特性。这两个看起来不同的定义都源自于我们对B"{u}chi自动机的共代数建模。基于这些共代数观察，我们还证明了它们的有效性：模拟确实证明了语言包含关系。
作者：Natsuki Urabe and Ichiro Hasuo
论文ID：1606.04680
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-06-22