并发计算是本质上不同于顺序计算的客观现象。许多并发计算模型相继被提出,试图能够像经典计算模型刻画顺序计算那样刻画并发计算。但是这些模型在许多方面缺乏统一的共识,比如基本运算符、操作语义、等价关系等等。这给并发计算的研究带来许多不便,特别是在程序等价、表达能力、图灵完备等领域,而这些又都是最基本的问题。进程演算是一类并发计算模型的统称。它们的共同特点是以通信为基础,使用交错式并发语义等。前面所提到的问题在进程演算中尤为明显,具体表现为许多不同但又相似的演算模型,繁多的等价关系以及不一致的表达能力比较结果等。交互理论正是为了给进程演算一个统一的框架而提出的。它把交互作为最基本的概念,在此基础上定义其他概念。本文的主要工作是在交互理论下重新研究了移动演算中的传名演算。作为交互理论的一个实例,我们重新研究了π演算,重点考察了其上模型独立的等价关系和证明系统。我们还在公平灰箱演算中引入测试等价,并考察了它的一些性质。具体说来,本文从如下几个方面得到了一系列有关交互理论和模型独立观测理论的成果和创新:?π演算上的观测理论研究本文把传名演算的代表π演算在交互理论下进行再研究,主要是考察了其上的各种模型独立等价关系,包括引入新的测试等价。根据交互理论,进程行为的等价性判断应该是只能靠环境与其的交互,也就是环境对进程的观测来达到的。因而对于等价关系的研究我们称为观测理论,绝对等价在π演算中的形式也称为观测等价。我们的π演算将名区分为(常量)名和名变量。操作语义和等价关系的定义则遵照了交互理论的基本原则。这个新模型的表达能力不弱于原来的π演算,但是有着更加漂亮的理论结果和更好的实际应用价值。本文论证了在原来的π演算上的不同等价关系(barbed互模拟、标号互模拟、开互模拟、准开互模拟)都等同于由交互理论基本原则出发定义的观测互模拟。于是我们得到一个更一致的π演算,并且它的理论被大大简化。测试等价也以一种略有不同但更符合交互理论的形式被引入,它严格包含观测等价,符合直观,有着更好的性质。?证明系统的研究公理系统的研究始终是伴随着进程演算发展的。正因为等式公理给出了有关进程等价的代数规则,故进程演算又被称为进程代数。在本文中,研究对象称为证明系统而不是公理系统,是因为本文不是对某一等价关系进行公理化,得出一套等式公理,而是借公理系统的研究得到一套能够证明两个进程相等的系统推理方法。我们将在我们的π演算上,对观测等价和测试等价在有限进程上的证明系统进行考察。为了方便公理化,我们在π演算上引入了选择操作子,但这样会导致观测等价不同余,因为观测等价不在选择操作子下封闭。但是我们发现了P与Q观测等价当且仅当τ.P和τ.Q在公理系统中可证相等,这就给我们提供了一套观测等价的证明方法。我们对测试等价作了相似的研究,也得到了一套证明系统。本文还就有限控制进程的测试等价作了考察。通过进程方程组的刻画,同样给出了有限控制进程上的测试等价的证明系统。?在公平灰箱演算上引入测试等价公平灰箱演算(Fair Ambient,简称FA)是灰箱演算家族的成员之一。它通过在原有的移动灰箱演算(MobileAmbient)中加入补名,加强了对灰箱移入移出的控制。曾经有人研究过灰箱演算上的上下文等价,这是may测试等价的变体,是一种比较弱的等价关系。本文中定义的测试等价充分利用了补名的作用,也就是充分利用交互的性质,使得一部分特殊形式的测试者拥有所有测试者的区分能力。它在有限进程上是一个同余关系,在一类后继终止的进程上严格包含互模拟等价。本文还考察了两种不同的对成功状态的定义,一种是从结构的观点,另一种是从交互的观点。这两种定义得到的是相同的测试等价,这在某种程度上表明了交互理论的合理性。本文还就从π到FA的翻译在测试等价的意义下是否完全抽象作了研究,结果表明这个翻译仍然保持完全抽象。这为π演算是公平灰箱演算的一个子演算的观点增加了重要砝码。本文对交互理论下的模型独立移动演算理论的所得到的研究成果,能够帮助人们深入理解交互理论。我们的π演算可以认为是在交互理论下重新认识进程演算的第一个实例,而对等价关系的研究表明进程演算中的等价关系能够统一到一个更加客观,独立于模型的关系。对于box等价的研究也显示出原本出发点很不相同的测试理论可以被很好地纳入交互理论。这些为进一步用交互理论研究进程演算、研究并发计算提供了非常有意义的尝试。