随着计算机技术和网络通信技术的高速发展，分布式并发系统已成为当前计算机技术的主流方向。相对于传统的串行计算机系统，分布式并发系统非常复杂，其开发过程不仅难度大，效率低，周期长，而且很难避免和发现其中隐含的错误和缺陷。形式化方法被公认为是一种行之有效的减少设计错误、提高系统可信度的重要途径。以CCS和π演算为代表的的进程代数方法是一类非常重要的形式化方法，因其概念简洁，可用的数学工具丰富，在并发系统的规范、分析、设计和验证等方面获得了广泛应用，而π演算已经发展为并发计算模型的典范，本文就是围绕π演算展开研究。在对π演算的研究中，进程的等价性问题一直是个核心问题，即在何意义下，两个语法形式不同的进程表达式可以认为是行为等价的。互模拟等价是π演算中最常见的等价关系，对其进行公理刻画是一个非常重要的研究方向。在给π演算赋予类型系统后，互模拟等价关系发生了变化，在新的环境下对π演算中的互模拟等价进行公理刻画是本文的主要工作。具体地，本文主要的研究内容和成果如下： 1.为了深刻理解π演算中互模拟等价的公理化体系，我们将π演算中的通道名和变量进行了区分，得到了π演算的一个变例，给出了这个变例的开互模拟等价关系的定义并对其进行了公理化，其定义相对原始定义更为简单。 2.类型系统对于并发计算模型的作用越来越得到人们的重视。我们以多元x演算为例，阐明并发计算模型中类型系统的作用。多元x演算允许一次通信交换多个名，在具有了更强的控制能力的同时也使得x演算在运行时会出现通信错误。我们赋予多元x演算一个递归类型系统，并证明此类型系统可以保证多元x演算不会出现通信错误。 3.能力类型是π演算中研究得最多的一种类型系统。能力类型允许我们区分通道的读写能力。类型化的互模拟等价关系，可以用基于“格局(configurations)”的标号转移系统给出定义。我们对类型化的开互模拟关系进行了研究，给出了此互模拟关系的一个完备的公理化系统。 4.一般的类型系统限制了程序设计时的灵活性。多态类型系统允许某个操作可以作用到不同类型的参数上，从一定程度上克服了这样的问题。在给π演算赋予多态类型系统后，环境只知进程中通道的抽象类型，此时，互模拟等价关系发生了变化。我们对多态π演算中的互模拟等价关系进行了研究，给出了其中互模拟等价关系的一个完备的公理化系统。