模态互模拟

互模拟是一场双方都能继续应答的逐步游戏。挑战者任选一边走一条可达边，另一边必须走到一个仍相关的世界；每到一对世界，原子观察必须相同。只要应答能无限继续，基本模态语言就找不到区分双方的公式。

forth 与 back 都不可少。只有 forth 的模拟适合表达单向行为包含，却可能让右侧拥有左侧无法回应的新分支；方框公式会观察这些额外分支。互模拟要求双向覆盖所有可见选择，才保证整套方框与菱形语言不变。

模型 $\mathcal{M}$ 的根 $w$ 有两个终止后继 $a,b$，两者都满足且只满足原子 $p$；模型 $\mathcal{N}$ 的根 $v$ 只有一个终止后继 $c$，且 $c$ 也满足 $p$。令

从 $w$ 走向 $a$ 或 $b$，$v$ 都可用同一个 $c$ 回应；从 $v$ 走向 $c$，$w$ 可任选 $a$ 回应。终止点没有后续挑战，原子也一致，所以两根互模拟。模态逻辑因此看不出“有两个相同后继”与“只有一个后继”的区别，说明它没有直接计数分支的能力。

若把 $b$ 上的 $p$ 改为假，原来的 $Z$ 违反原子一致；公式 $\square p$ 也区分两根：它在 $v$ 真、在 $w$ 假。若仅删除 back 条件，还可能把一个只有安全分支的模型模拟进另一个另含危险分支的模型，错误地声称方框性质保持。

模态等价反向推出互模拟需要条件。在像有限（image-finite，即每个世界只有有限多个后继）模型中，Hennessy–Milner 定理给出：满足相同基本模态公式的两个世界必互模拟。对任意无限分支模型，模态等价可能没有单个互模拟关系见证；模态饱和等更强条件可恢复反向。

互模拟是不变性与表达力分析的标准尺度。若一个世界性质在互模拟下不保持，它就不能由基本模态公式定义；“根恰有两个后继”正是例子。加入计数模态或混合逻辑命名后，通常需要加强匹配条件；模态 $\mu$-演算虽然加入不动点，仍在普通互模拟下保持不变，但证明还须处理不动点语义。

在状态系统验证中，互模拟商可以合并行为等价状态并保留模态规格。算法实际计算的常是最大互模拟或分区精化；正确性需要证明所得分区满足原子、forth、back，而不是只比较节点标签或出度。

过滤法公理库Kripke 模型过滤法Kripke model filtration · Filtration method in modal logic按有限公式集的真值类型合并世界，并在商模型中保持这些公式满足性的有限化方法。按有限公式集真值合并状态，得到的是相对于 $\Sigma$ 的有限不可区分；互模拟则保证全部基本模态公式不变。前者依赖选定公式集并给出指数状态界，后者不依赖 $\Sigma$，但商后是否有限取决于原模型。