互模拟

双向逐步匹配 ​

设 ${\mathcal{L}}_1,{\mathcal{L}}_2$ 共享动作字母表。关系 $R\subseteq S_1\times S_2$ 是强互模拟，若对每个 $(s,t)\in R$、每个标签 $a$ 同时满足：

$$s{\stackrel{a}{\to }}_1{s}^{\prime }⟹\mathrm{\exists }{t}^{\prime },t{\stackrel{a}{\to }}_2{t}^{\prime }\wedge (s^{\prime },t^{\prime })\in R,$$$$t{\stackrel{a}{\to }}_2{t}^{\prime }⟹\mathrm{\exists }{s}^{\prime },s{\stackrel{a}{\to }}_1{s}^{\prime }\wedge (s^{\prime },t^{\prime })\in R.$$

若存在包含 $(s,t)$ 的互模拟，称 $s,t$ bisimilar，记 $s\sim t$。在固定标号转移系统上，bisimilarity 是等价关系公理库等价关系Equivalence relation满足自反、对称和传递性的关系。，可据此把状态空间商掉。

它不是把两份单向模拟公理库模拟关系Simulation relation · Forward simulation · Weak simulation用方向性的状态关系要求一个系统的每步行为能够由另一个系统匹配。陈述并排抄写：关键是每次匹配后的后继仍落在同一关系中，使未来所有分支可以继续相互回应。

售货机状态的配对 ​

系统 A 收到 coin 后进入 $a_1$，再执行 tea 回到初态。系统 B 收到 coin 后先进入 $b_1$，做一个内部实现步骤，再到 $b_2$，最后执行 tea。

在强语义下，A 没有动作匹配 B 的内部步，因此相应状态不强互模拟。若该内部动作标作 $\tau$ 并采用弱互模拟，A 可以用零步匹配它，关系可包含

$$(a_0,b_0),(a_1,b_1),(a_1,b_2).$$

可见 coin tea 行为被保留，而内部实现阶段被隐藏。若 B 在 $b_1$ 还能执行可见 refund，A 必须从 $a_1$ 提供相同可见选择，否则双向条件失败。

这个例子展示互模拟检查的是分支菜单，不仅是已经走出的一条动作串。

比轨迹等价更细 ​

考虑系统 P 在开始时内部选择“以后只做 $a$”或“以后只做 $b$”，系统 Q 则在每次可见选择点同时允许 $a,b$。在适当有限轨迹语义下，两者都可能产生 $a$ 或 $b$，轨迹集合可以相同。

但分支时机不同：P 的内部选择一旦完成，环境看到的可用菜单只剩一个动作；Q 仍保留两个。互模拟必须逐状态匹配所有出边，因此能够区分它们。

一般有

$$s\sim t⟹\mathrm{Traces}(s)=\mathrm{Traces}(t),$$

反向不成立。若系统确定且满足额外条件，某些行为等价可能重合，但不能把特殊情形写成普遍结论。

协归纳证明方式 ​

要证明 $s\sim t$，通常提出候选关系 $R$，再逐类检查关系中状态对的所有出边都能匹配。这是协归纳：不展开所有无限执行，而是证明关系在一步观察下封闭。

最大互模拟可以看作关系变换器的不动点。令 $\mathrm{\Phi }(R)$ 收集在 $R$ 下能双向匹配一步的状态对，则 bisimilarity 是 $\mathrm{\Phi }$ 的最大不动点。选择最大而非最小不动点，允许无限行为通过持续匹配获得证明。

仅画一个循环箭头并说“两边都能一直走”不是证明。若标签、分支数或终止状态有一处不匹配，候选关系就不闭合。

反证不等价时，可用有限深度的区分游戏：攻击者在任一系统选择一步，防守者必须在另一系统以同标签回应；若防守者有限轮内无路可走，攻击策略就给出非互模拟见证。有限状态系统上，逐轮删除不能匹配的状态对最终稳定，所得最大关系正是 bisimilarity，也给出可执行判定过程。

弱互模拟的边界 ​

弱互模拟用 ${\tau }^{\ast }a{\tau }^{\ast }$ 匹配可见动作，并允许内部步被若干内部步或零步匹配。不同定义还会区分 branching bisimulation、delay bisimulation 与观察同余；它们对分支在内部步前后何时保存有不同要求。

弱 bisimilarity 未必在所有进程组合操作下都是 congruence。若要用等价状态替换一个组件而保持整体行为，需要检查所用语言算子与等价关系的相容定理。

互模拟也不会保留未纳入观察的性能、概率或实时性质。两个系统动作结构相同，但一个 tea 需一秒、另一个需一小时，在无时间标签的 LTS 中仍可能互模拟。

把互模拟商用于状态约简时，应让每个等价类作为新状态，并由任一代表的标签转移诱导商转移。双向匹配保证代表选择不改变可见后继类；若只按“拥有同一状态标签”分组，两个节点的未来分支可能不同，所得商图会合并不等价行为。

参考资料

• Robin Milner, Communication and Concurrency, Prentice Hall, 1989, Chs. 4–5。
• Davide Sangiorgi, Introduction to Bisimulation and Coinduction, Cambridge University Press, 2012, Chs. 1–4。
• J. C. M. Baeten, “A Brief History of Process Algebra,” Theoretical Computer Science 335(2–3), 2005, pp. 131–146。