一句话：用 Spoiler-Duplicator 博弈统一刻画分支、延迟、η 与弱双模拟，并辅助诊断实现与规约的不一致。
在进程代数中，弱双模拟通过静默步抽象内部行为，用于将实现与规约关联；但当实现不符合规约时，定位根因往往困难。本文给出了分支双模拟、延迟双模拟、η-双模拟和弱双模拟的一种统一博弈刻画，将其表示为 Spoiler 与 Duplicator 之间的博弈，从而提供这些关系的操作式理解。作者进一步展示如何利用此类博弈辅助诊断实现与规约之间的不一致，并说明如何扩展博弈以区分发散。该工作为双模拟提供了一种通用的博弈视角，有助于理解与调试进程代数中的一致性关系。
Weak bisimulations are typically used in process algebras where silent steps are used to abstract from internal behaviours. They facilitate relating implementations to specifications. When an implementation fails to conform to its specification, pinpointing the root cause can be challenging. In this paper we provide a generic characterisation of branching-, delayed-, $\eta$- and weak-bisimulation as a game between Spoiler and Duplicator, offering an operational understanding of the relations. We show how such games can be used to assist in diagnosing non-conformance between implementation and specification. Moreover, we show how these games can be extended to distinguish divergences.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{EscrigKW16,
title = {Games for Bisimulations and Abstraction},
author = {David De Frutos Escrig and Jeroen J. A. Keiren and Tim A. C. Willemse},
journal = {Logical Methods in Computer Science},
volume = {Volume 13, Issue 4},
year = {2017},
doi = {10.23638/lmcs-13(4:15)2017}
}