Bisimulation

定义 Definition

bisimulation（双模拟）：在理论计算机科学（尤其是并发理论、过程代数、模型检验）中，用来判定两个状态/系统是否“行为等价”的一种关系。直观地说，如果系统 A 走一步能到某个状态，系统 B 也能走一步到“对应”的状态，反过来也一样，则它们在该关系下是双模拟的。（在不同语境中还可能涉及强/弱双模拟等变体。）

例句 Examples

Two labeled transition systems are equivalent if there exists a bisimulation between their initial states.
如果两个带标记的转移系统的初始状态之间存在一个双模拟关系，那么它们是等价的。

In the verification of concurrent protocols, bisimulation provides a robust notion of behavioral equivalence that is preserved under composition.
在并发协议的验证中，双模拟提供了一种稳健的行为等价概念，并且在组合（合成）操作下仍能保持。

发音 Pronunciation (IPA)

/ˌbaɪsɪmjuːˈleɪʃən/

词源 Etymology

由 bi-（“双、两者”）+ simulation（“模拟”）构成，字面意思是“双向的模拟”：不仅 A 能模拟 B 的行为，B 也能反过来模拟 A 的行为，因此用于刻画“你来我往都对得上”的行为一致性。

相关词 Related Words

• Equivalence
• Simulation
• Isomorphism
• Congruence
• Refinement
• Coinduction
• Bisimilar
• Lts

文学与经典著作 Literary Works

• Communication and Concurrency（Robin Milner）：在并发理论语境中系统讨论双模拟等行为等价概念。
• The π-Calculus: A Theory of Mobile Processes（Davide Sangiorgi & David Walker）：在 π 演算中广泛使用双模拟来刻画过程等价。
• Principles of Model Checking（Christel Baier & Joost-Pieter Katoen）：在模型检验框架下介绍双模拟及其与等价缩减等技术的关系。
• Model Checking（Edmund M. Clarke, Orna Grumberg, Doron A. Peled）：在形式化验证语境中提及与双模拟相关的等价与简化思想。