[科普中国]-互模拟等价

互模拟等价就是两个系统能够相互模仿对方 ,从而从观察者的角度讲 ,在某种程度上 ,它们是行为等价的。因此 ,互模拟等价是描述行为等价的一个数学概念 ,它从某个侧面反映客观世界两个系统行为之间的关系。互模拟等价可定义在各种结构上1。

发展背景在上世纪80年代左右,人们在计算机科学、模态逻辑和集合论中大体上是同时并且独立地发现互模拟。无论是在计算机科学中,还是在模态逻辑和集合论中,互模拟等价都是通过对代数结构之间态射概念进行提炼而产生。最基本的态射形式是同态,它给予了我们把一个结构(源结构)嵌入另一个结构(目标结构)的方式,使得源结构中的所有关系保持在目标结构中。然而,它的逆不一定成立;鉴于此,需要更强的态射概念。而常用的一个这样的概念是同构,然而同构的概念又太强,因为同构的结构本质上和形式上都是相同的。于是，人们希望有一个介于同态和同构之间的概念，在这一探索过程中，互模拟等价被引入1。

互模拟等价定义模态逻辑中常常把互模拟定义在克里普克模型上。

定义 令 M = (W , R, V ) 和 M ′= (W ′, R′,V′)是两个克里普克模型 ,令 Z∈W ×W ′是一个非空的二元关系 , 对于任意的 w ∈W , w′∈W ′, 如果wZw′,那么

( i)对所有命题字母 p, w∈V (p)当且仅当 w′∈V′(p) ;

( ii)对于所有的 v∈W ,如果 Rwv,那么存在 v′∈W ′使得 R′w′v′,并且 vZv′; (向前 )

( iii) 对于所有的 v′∈W ′,如果 R′w′v′,那么存在 v∈W 使得 Rwv,并且 vZv′。 (向后 )

则我们称 Z是模型 M到模型 M ′上的一个互模拟1。

互模拟等价性质互模拟具有三个主要的性质，可以根据互模拟定价的定义进行推到得到：

（1）自返性

（2）对称性

（3）传递性

互模拟等价应用模态逻辑中的应用互模拟等价被广泛地运用于模态逻辑的研究中,比如用它去分析其他类型模态逻辑的表达力,如Janin和Walukiewicz证明了μ-演算对应于MSO的互模拟不变的一部分;用它去说明什么样的模型特征在模态逻辑中是可以表达的;用它来定义在模型上保持模态公式有效性的运算;在模型检测中互模拟用来收缩模型,同时还保持模型的语义。2

计算机科学中的应用在理论计算机科学中,互模拟等价关系被运用于标号迁移系统3。标号迁移系统被用来描述进程:标号迁移系统中的结点被解释为进程的可能状态,标号迁移系统中的一元关系被解释为状态性质;标号迁移系统中的二元关系被解释为进程可能执行的原子行为。互模拟等价及其变体可被看作标号迁移系统上的等价关系:两个互模拟的标号迁移系统描述了相同的进程。4

并发系统中的应用互模拟等价因为各种目的被广泛地用在并发系统中:·最大互模拟等价一般被看作是施加于系统上的最精致的行为等价性。

互模拟等价证明方法被用来证明过程之间的等价性。

利用最大互模拟等价检测算法的效力和最大互模拟合成性特征使进程的状态空间最小化。

最大互模拟等价和它的变体被用来对某些系统进行抽象化5

本词条内容贡献者为:

王沛 - 副教授、副研究员 - 中国科学院工程热物理研究所