一句话：从余代数视角统一推广 Büchi 自动机的公平模拟至非确定树自动机与概率字自动机，并证明其可靠性。
模拟关系为语言包含提供了一种可计算且可靠（但不必然完备）的证明方法。已有工作研究了非确定/实时系统的模拟以及 Büchi 自动机的公平模拟。本文从余代数视角统一建模 Büchi 自动机，并将公平模拟推广到两个方向：非确定树自动机，以及有限状态概率字自动机，二者均采用 Büchi 接受条件。非确定定义以不动点方程组给出，可转化为 parity game 并适合 Jurdziński 算法；概率定义则带有强烈的 ranking function 风格。作者证明这两种表面不同的定义源自同一余代数结构，并证明其可靠性：若存在模拟关系，则它确实见证语言包含。
Notions of simulation, among other uses, provide a computationally tractable and sound (but not necessarily complete) proof method for language inclusion. They have been comprehensively studied by Lynch and Vaandrager for nondeterministic and timed systems; for B\"{u}chi automata the notion of fair simulation has been introduced by Henzinger, Kupferman and Rajamani. We contribute to a generalization of fair simulation in two different directions: one for nondeterministic tree automata previously studied by Bomhard; and the other for probabilistic word automata with finite state spaces, both under the B\"{u}chi acceptance condition. The former nondeterministic definition is formulated in terms of systems of fixed-point equations, hence is readily translated to parity games and is then amenable to Jurdzi\'{n}ski's algorithm; the latter probabilistic definition bears a strong ranking-function flavor. These two different-looking definitions are derived from one source, namely our coalgebraic modeling of B\"{u}chi automata. Based on these coalgebraic observations, we also prove their soundness: a simulation indeed witnesses language inclusion.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{UrabeSH16,
title = {Fair Simulation for Nondeterministic and Probabilistic Buechi Automata: a Coalgebraic Perspective},
author = {Natsuki Urabe and Ichiro Hasuo},
journal = {Logical Methods in Computer Science},
volume = {Volume 13, Issue 3},
year = {2017},
doi = {10.23638/lmcs-13(3:20)2017}
}