互模拟

售货机状态的配对 ​

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

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

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

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

比轨迹等价更细 ​

取两个完全明确的有限系统。$P$ 的初态只有一条 $a$ 边到 $p$，$p$ 再分别通过 $b$、$c$ 到达停止状态。$Q$ 的初态有两条 $a$ 边：一条到只允许 $b$ 的 $q_b$，另一条到只允许 $c$ 的 $q_c$，随后也停止。

若有限 trace 包含所有可执行前缀，两者恰有相同集合 $\{\epsilon ,a,ab,ac\}$。但它们不强互模拟：匹配 $P$ 的 $a$ 步时，$Q$ 无论选 $q_b$ 还是 $q_c$，都无法同时匹配 $p$ 保留的 $b,c$ 两种出边。区别是选择发生在 $a$ 之前还是之后；这里没有借用未说明的“短轨迹”限制来掩盖更长行为。

一般有

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

协归纳证明方式 ​

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

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

仅画一个循环箭头并说“两边都能一直走”不是证明。若一方的某条出边找不到同标签、且后继仍在 $R$ 中的回应，候选关系就不闭合。这种匹配不要求一一对应：两条边可以由同一条边回应，因此出边条数不同的状态仍可能互模拟。

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

弱互模拟的边界 ​

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

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

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

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

给迁移加上概率之后，概率互模拟理路概率互模拟Probabilistic bisimulation按等价类总转移概率定义有限 Markov 链的强互模拟，算出可合并状态并展示概率差异如何被观察。要求相关状态到每个等价类的总转移质量相同。逐个原状态的质量可以不同，只有相同出边支撑却不够；这一条件使商 Markov 链不依赖类代表，并保留相应可观察概率。