模拟关系

一步模拟的方向 ​

设两个标号转移系统公理库标号转移系统Labeled transition system · Labelled transition system · LTS在状态转移上标记动作，明确路径、可达性、使能动作以及终止与死锁的行为模型。

$$\mathcal{C}=(S_C,I_C,A,{\to }_C),\mathcal{A}=(S_A,I_A,A,{\to }_A).$$

关系 $R\subseteq S_C\times S_A$ 是从具体系统到抽象系统的强模拟，若每个具体初始状态都能关联某个抽象初始状态，并且

$$\mathrm{\forall }(c,a)\in R,\mathrm{\forall }\ell \in A,\mathrm{\forall }{c}^{\prime },c{\stackrel{\ell }{\to }}_C{c}^{\prime }⟹\mathrm{\exists }{a}^{\prime },a{\stackrel{\ell }{\to }}_A{a}^{\prime }\wedge (c^{\prime },a^{\prime })\in R.$$

量词次序很重要：对具体系统的每一步，抽象系统可以选择一个匹配后继。不能先固定一个 $a^{\prime }$ 再要求它匹配所有不同具体步骤。

若这样的关系存在，写作 $\mathcal{C}⪯\mathcal{A}$。方向表示抽象系统至少允许具体系统的行为；文献也有反向记号，使用时必须同时写出匹配条件。

一条状态配对轨迹 ​

具体计数器状态为整数 $n$，动作是 inc，转移 $n\stackrel{inc}{\to }n+1$。抽象系统只记录奇偶状态 $E,O$，并有

$$E\stackrel{inc}{\to }O,O\stackrel{inc}{\to }E.$$

令 $R$ 把偶数关联 $E$、奇数关联 $O$。从配对 $(2,E)$ 出发，具体步 $2\to 3$ 由 $E\to O$ 匹配，新配对为 $(3,O)$；下一步 $3\to 4$ 由 $O\to E$ 匹配。

该关系覆盖每个整数和唯一奇偶摘要，且每步封闭，因此给出模拟。抽象状态遗忘计数器大小，却保留 inc 交替改变奇偶性的行为。

若抽象系统遗漏 $O\to E$，第一步仍能匹配，第二步便失败。展示一段成功前缀不能证明模拟，条件必须覆盖关系中的全部状态和全部具体出边。

可见性质与行为包含 ​

沿模拟关系逐步选择匹配后继，可用路径长度归纳证明：每条具体有限动作轨迹也是抽象轨迹。对无限轨迹还要依赖逐步选择或适当的路径构造条件。

因此抽象系统若满足对所有轨迹封闭的安全性质，具体系统也满足它。不过这项传递依赖性质只观察被模拟保留的标签或状态命题。若抽象状态没有保存 balance<0，不能从模拟关系凭空推出余额性质。

抽象系统可以拥有额外行为，所以反方向通常不成立。抽象模型发现反例时，它可能只走了具体系统无法实现的路径；这就是 abstraction refinement 要排除的伪反例来源。

若状态还带原子命题，关系通常另要求相关状态满足相同观察，或至少让具体命题蕴含抽象命题。否则可以把所有具体状态关联到一个没有任何标记的抽象自环，动作匹配形式上成立，却无法传递待证状态性质。模拟证明必须同时写出转移和观察的保存义务。

弱模拟与内部步骤 ​

若标签集含内部动作 $\tau$，强模拟要求连每个内部微步也逐一匹配，可能过于严格。定义弱转移

$$a\stackrel{\ell }{\Rightarrow }{a}^{\prime }$$

表示若 $\ell \ne \tau$，可先走若干 $\tau$、走一次 $\ell$、再走若干 $\tau$；若 $\ell =\tau$，通常允许零步或多步内部转移。弱模拟把匹配条件中的单步抽象转移换成弱转移。

允许零步匹配会隐藏实现细化出的内部工作，但也可能掩盖 divergence：具体系统无限执行 $\tau$ 而永不产生可见动作，抽象系统若一直零步匹配，就无法区分忙等与终止。divergence-sensitive 变体需另加条件。

预序而非自动等价 ​

模拟关系具有方向性。恒等关系给出自反性，两个模拟关系的关系复合给出传递性，所以系统间“存在模拟”通常形成预序；不同系统可能互相模拟但不是同一个语法对象。

只存在 $\mathcal{C}⪯\mathcal{A}$ 不能推出二者行为等价。若要求同一关系双向匹配每一步，就得到更强的互模拟。单独找到反向另一份模拟也需检查它们保留的观察和内部动作约定是否一致。

模拟还不同于测试若干对应状态。关系公理库关系Relation · Binary relation带源集与目标集的二元关系，其底层关系图是 A×B 的子集。可以一对多、多对一；证明责任是初始覆盖和逐步闭包，而不是构造一个看似自然却未验证的映射。

参考资料

• Robin Milner, Communication and Concurrency, Prentice Hall, 1989, Chs. 4–5。
• Nancy A. Lynch and Frits W. Vaandrager, “Forward and Backward Simulations,” Information and Computation 121(2), 1995, pp. 214–233。
• Davide Sangiorgi, Introduction to Bisimulation and Coinduction, Cambridge University Press, 2012, Chs. 1–2。