互模拟的一些基本性质，本文主要内容关键词为：性质论文，此文献不代表本站观点，内容供学术参考，文章仅供参考阅读下载。
[中图分类号]B815 [文献标识码]A [文章编号]1000-5110(2010)05-0068-06
一、引言
从直观上讲，互模拟就是两个系统能够相互模仿对方，从而从观察者的角度讲，在某种程度上，它们是行为等价的。在上世纪80年代左右，人们在计算机科学、模态逻辑和集合论中大体上是同时并且独立地发现互模拟。无论是在计算机科学中，还是在模态逻辑和集合论中，互模拟都是通过对代数结构之间态射概念进行提炼而产生。最基本的态射形式是同态，它给予了我们把一个结构(源结构)嵌入另一个结构(目标结构)的方式，使得源结构中的所有关系保持在目标结构中。然而，它的逆不一定成立；鉴于此，需要更强的态射概念。而常用的一个这样的概念是同构，然而同构的概念又太强，因为同构的结构本质上和形式上都是相同的。于是，人们希望有一个介于同态和同构之间的概念，在这一探索过程中，互模拟被引入。[1]
互模拟理论在模态逻辑、集合论和计算机科学中已经发挥了日益重要的作用。在模态逻辑方面，自从Benthem定理问世之后，互模拟被广泛地运用于模态逻辑的研究中，目前已成为模态逻辑模型论的一个核心概念；可以使用互模拟证明内插定理等重要定理；使用互模拟证明一些模态逻辑的表达力；用它去解释什么样的模型性质是模态可定义的；用它来定义在模型上保持模态公式有效性的运算；使用互模拟构造商模型等等。
互模拟理论也是非良基集合论的核心。当人们把集合的论域由良基集合扩展到非良基集合时，经典的外延公理在判断非良基集合之间的相等性方面显得无能为力，运用基于互模拟概念的强外延公理可以很好地解决这一问题。互模拟也可以定义在图上或方程组上，通过图之间或方程组之间的互模拟关系，可以间接地判断集合之间的等价性。最早为标准集合论设计的各种可满足性的判定算法在非良基集合论中有它们的对应算法。在这里，属于关系以所有可能的方式违反了良基性，然而基于互模拟的限制原则避免了论域中个体的过分繁殖。另外，互模拟还被用来判断由某个集合A生成的流之间的相等性，用来证明后继函数的单射性质以及被用来刻画序数等等。[2][p.77-78]
今天，互模拟理论因为各种目的被广泛地用在并发系统的研究中，如：最大互模拟一般被看做是施加于系统上的最精致的行为等价性；互模拟证明方法被用来证明进程之间的等价性；利用最大互模拟检测算法的效力和最大互模拟合成性特征使进程的状态空间最小化；最大互模拟和它的变体被用来对某些系统进行抽象化。互模拟和由它生成的共归纳技术被运用于许多领域，如：函数语言、对象定位语言、类型论、数据类型、域论、数据库、编辑最优化、程序分析、证明工具等等。随着互模拟不断地被用到新的形式化理论中，这对于逻辑学，特别是哲学逻辑的进一步发展将会起到更大的促进作用。
二、互模拟的定义
加标转换系统LTS是描述一个系统可能产生的交互的最常用的结构。在计算机的并发系统中，计算就是交互。例如，进入一个记忆单元，访问一个数据库，在一台洗衣机中选择一个程序。一个交互的参与者就是进程(在洗衣机的例子中，洗衣机和选择程序的人就是被涉及的进程)。一个进程的行为应该告诉我们进程和外部世界在什么时候交互以及怎样交互。因此，我们首先需要一个适当的方法来描述一个进程的行为。
交互的另一个例子是能够卖茶和咖啡的自动售货机。[3][p.16]机器有一个投钱的狭孔，一个是索要咖啡的按钮，另一个是索要茶水的按钮，还有一个收藏送来的饮料的空间。机器的行为就是我们通过与机器交互能够看到的东西。这意味着用机器进行试验活动：按按钮并看看发生了什么。我们能够看到的是哪个按钮何时按下去了，和我们何时能得到什么饮料。其他的每件事情，比如机器的颜色和形状是不相关的。我们能够把与机器行为相关的东西描述成一个加标转换系统，如图1所示。
图1 自动售货机的模型
一个加标转换系统告诉我们一个系统可能处于什么状态，以及从每一个状态开始的可能的交互。一个交互用一个加标的直线表示；用加标转换系统的术语来说，它被称为转换。在图1自动售货机里，存在4个状态。开始机器处于状态
。与
之间的标有1元的转换表示在状态，机器接受了一个硬币，并因此进入了状态；在中进一步有两种可能转换，一种转换表示要咖啡，另一种转换表示要茶叶；如此等等。
下面再给出一个与图1自动售货机有相同语言的另一台售货机的模型(见图2)。[3][p.16]
虽然这个自动机与上一个自动机有相同的语言，也就是和
有相同的路径集，但是在一个办公室里，拥有第一台机器和拥有第二台机器的确不一样。当我们把硬币投入图2描述的机器时，结果状态可能是
，也可能是
，机器的非确定性决定了我们无法控制这一点。结果，如果我们想要一杯饮料，我们必须接受机器提供给我们的任一饮料。与此不同的是，图1描述的机器总是让我们选择我们最喜欢的饮料。这就说明这两个自动机不是行为等价的，更具体地说，虽然和是语言等价(路径等价)的，但是与它们进行交互可能导致迥异的结果，这说明，正如同态不能用来刻画状态的行为等价性一样，路径等价性也不能用来刻画进程的行为等价性；所以进程的路径等价性不能用来刻画进程的行为等价性；同时，数学中的同构、强同态，以及模态逻辑的有界态射，虽然可以用来判断一些进程之间的行为等价性，但是这些概念使用的是加标转换系统之间的函数关系，这就把许多实际上是行为等价的进程(结构)排除在行为等价类之外，因此需要寻找合适的描述进程的行为等价性的概念，这一动机直接导致了互模拟的诞生。
标签：电脑论文;