一句话：提出统一博弈，可在 van Glabbeek 线性时间—分支时间谱系中一次性判定两进程的行为等价关系。
论文研究有限状态进程之间的行为等价判定：van Glabbeek 的线性时间—分支时间谱系包含多种粗细不同的等价与前序，传统方法需逐一判定。作者推广了互模拟博弈，使其能从该谱系中每个有限、对子公式封闭的逻辑片段中构造出区分两进程的 Hennessy–Milner 逻辑公式。他们识别了刻画表达力的关键维度，从而保证所得公式属于能够区分两进程的最粗行为前序或等价。作者进一步证明，由该博弈诱导的算法能够一次性确定一对进程在谱系中各等价关系上的最佳匹配，即精确判断它们在哪些（不）等价下相同或不同。
We introduce a generalization of the bisimulation game that finds distinguishing Hennessy-Milner logic formulas from every finitary, subformula-closed language in van Glabbeek's linear-time--branching-time spectrum between two finite-state processes. We identify the relevant dimensions that measure expressive power to yield formulas belonging to the coarsest distinguishing behavioral preorders and equivalences; the compared processes are equivalent in each coarser behavioral equivalence from the spectrum. We prove that the induced algorithm can determine the best fit of (in)equivalences for a pair of processes.
@article{paperbot1668,
title = {Deciding All Behavioral Equivalences at Once: A Game for Linear-Time--Branching-Time Spectroscopy},
author = {Benjamin Bisping and David N. Jansen and Uwe Nestmann},
journal = {Logical Methods in Computer Science},
volume = {Volume 18, Issue 3},
year = {2022},
doi = {10.46298/lmcs-18(3:19)2022}
}