，，

(1.福建工程学院 信息科学与工程学院，福建 福州 350118；2.福建省大数据挖掘与应用技术重点实验室，福建 福州 350118)

系统的行为等价性分析是一个困难且微妙的领域，即使两个系统具有相同的行为，但行为发生顺序的不同，也可能导致两个系统之间很大的差异，从而对外部产生不同的影响。在计算机科学领域，自动机理论是应对这一问题的有力工具[1-2]，它使用状态、动作和状态迁移来构建系统的形式化模型，通过分析自动机可接受的语言，来判断不同自动机的等价性[3]。进一步的研究发现，自动机语言的等价性并不意味着两个自动机完全等价[4]，并由此引入了互模拟的概念[5]。

互模拟本质上是一种态射形式[6]，是两个数学结构之间保持结构的过程抽象，比同态更强，但弱于同构。在系统行为的等价性分析中，互模拟可以理解为两个系统能够相互模仿对方，使得在观察者的角度，它们的行为是相同的。互模拟的概念与技术被应用到许多计算机科学的研究课题中，例如，函数语言、证明工具、程序分析等，是形式化理论的重要基础之一。

本文使用标号迁移系统构建了系统行为的形式化模型，并通过标号迁移系统的语言来规约系统行为序列，解释了语言等价不同于行为等价的原因。在此基础上，通过标号迁移系统构建了模拟及互模拟概念的形式化模型，进而给出了系统间的互模拟关系。最后，讨论并证明了模拟及互模拟关系的一些性质。……