分支双似性与弱跟踪语义之间能谱的能量游戏

我们提供了对 van Glabbeek 线性时间-分支时间光谱（含静默步骤）的首个通用游戏表征。通过这种方式，可以使用一个多维能量游戏来一次性 characterize 和决定在稳定性尊重的分支双似性与弱跟踪等价之间的广泛一组弱行为等价。为建立正确性，我们将攻击者获胜的能量预算与 Hennessy--Milner 逻辑中区分子语言联系起来，并通过八个维度的公式可表达性来表征这些子语言。