弱行为等价谱系的统一博弈刻画：从稳定性保持分支互模拟到弱迹等价

《Information and Computation》：Deciding all behavioral equivalences at once II: The silent-step spectrum

　　

研究人员提供了van Glabbeek含静默步的线性时间–分支时间谱系的首次广义博弈刻画。在定量表述中，一个多维能量博弈（multi-dimensional energy game）可用于一次性刻画并判定稳定性保持分支互模拟（stability-respecting branching bisimilarity）与弱迹等价（weak trace equivalence）之间广泛的弱行为等价关系。以该方式判定所有概念所需时间关于状态数为指数级。为确立正确性，研究人员将攻击者获胜的能量预算（attacker-winning energy budgets）与Hennessy–Milner逻辑（HML）的可区分子语言相关联，并通过公式表达力的八个维度（eight dimensions of formula expressiveness）对其进行刻画。

研究背景方面，为特定用例选择合适的行为等价概念十分困难。van Glabbeek的线性时间–分支时间谱系将众多等价关系组织为模态逻辑的层级结构，但其中处理静默τ步的弱等价部分仅有扩展摘要形式，缺乏系统化的判定手段，且弱谱系的模态逻辑相当复杂、不满足HML子项封闭性，现有弱互模拟博弈缺乏覆盖谱系中较弱概念所需观测的博弈动作。为此，研究人员开展本研究，旨在将静默步谱系操作化，使一个能量博弈能够一次性判定从稳定性保持分支互模拟到弱迹等价之间的广泛弱行为等价关系。研究得出，攻击者获胜能量预算与可区分公式价格精确对应，并由此获得各等价概念的判定程序与博弈刻画，这对并发理论中等价概念的选择与验证具有重要意义。关键技术方法包括：采用广义互模拟能量博弈（spectroscopy energy game），引入延迟观测、稳定合取与分支合取等模态；通过八维公式表达力度量对HML子语言定价；利用多加权递减能量博弈（declining energy game）的获胜预算进行计算；并在Isabelle/HOL中形式化核心结果；原型工具在equiv.io及CAAL扩展上实现。研究结果方面，第一，重新绘制了含静默步的弱行为等价谱系，通过HMLsrbb的八个表达力维度定义各观测概念，并证明坐标刻画与操作定义一致，涵盖弱/η/延迟/分支互模拟及其稳定性保持变体、反模拟、稳定互模拟及线性时间概念。第二，提出了静默步谱系的首个广义博弈刻画，通过延迟博弈、稳定性博弈与弱博弈三层扩展覆盖延迟观测、稳定合取与分支合取区分能力。第三，证明了正确性定理：存在价格不超过e的HMLsrbb公式区分p与Q，当且仅当攻击者以预算e在弱博弈中从[p,Q]a获胜。第四，给出了个体判定与一次性判定所有等价的方法，并通过实例说明工具输出可指导等价概念选择。第五，分析了指数复杂度，并提出简化博弈将分支合取的出度降至线性，结合能量格封顶进一步改进时空复杂度，同时证明了简化博弈的松弛正确性。讨论部分总结了本工作与Chen和Deng、Fahrenberg等及自身先前工作的关系，指出静默步谱系中多种互模拟抽象使问题更为复杂，本博弈首次显式考虑稳定性保持概念，统一了稳定与非稳定等价，并指出可扩展至发散敏感等更多概念。研究结论翻译：本文提供了弱行为等价与前序谱系的首个广义博弈刻画。为此，第2节引入了分支互模拟的新模态刻画，用于在第3节捕获静默步谱系的模态逻辑。在此视角下，弱等价问题族成为一个定量问题，可在第4节表达为一个能量博弈。如第6节所示，这可用于方便地解决并发理论研究任务，并可扩展至更多概念。得益于第7节的博弈简化，具有相当内部非确定性的有意义的实际模型可以被处理。