随着多线程并发计算在我们生活中越来越普遍,π演算作为一种重要的并发计算模型,被广泛地应用于动态系统的建模上。由于异步通信在许多并发系统中更为常见,例如分布式系统等,因此在同步π演算的基础上,衍生出了可以异步通信的异步π演算。针对二者表达能力的研究也应运而生,最常用的研究方法是转换编码。然而,受限于编码对名字的控制,现有的转换编码存在明显的不足之处:等价对象通过编码不一定能转换成等价对象,即不满足完全抽象性质。本文研究给出了一个基于异步π演算的子异步π演算,并构造了一个从同步π演算到该演算满足完全抽象性质的转换编码。本文对于子异步π演算的主要研究工作与贡献,包括以下三个方面:·在不改变异步π演算异步通信能力的基础上,构造了主名和辅名两种不同的名字,通过辅名加强了对演算归约顺序的控制。更进一步,研究了子异步π演算的动态特征,通过标号迁移系统给出了操作语义,完整构建了子异步π演算的模型体系。·定义了子异步π演算中的接口等价关系和互模拟关系。并在此基础上研究了up-to互模拟关系,降低了所需关系的规模。证明了子异步π演算中的互模拟关系为绝对等价关系,形成了一个完整的行为等价理论。通过该理论对表达能力研究中不同对象的等价关系进行分析与验证。·实现了同步π演算到子异步π演算的镜像版本转换编码,对应构造了演算间迁移的操作一致性,解决了原有编码不满足完备性的缺陷。并且利用行为等价理论和结构化定理严格证明了子异步π演算转换编码在互模拟关系下的完全抽象性质,并通过实例进行了验证。总的来说,本文提出的子异步π演算和对应编码加强了π演算中对名字的控制,并使多步归约更为可控。相应构建的演算构造规则,以及证明中使用的构造上下文和up-to互模拟等证明技术,为后续更进一步研究同步通信到异步通信的完全抽象编码提供了理论基础。