论文部分内容阅读
移动系统无处不在。传名演算，通常称为π演算，是由Milner、Parrow和Walker为了刻画移动系统提出的并发移动模型。π演算不仅是移动系统的基础模型之一，更是描述、分析系统和验证系统正确性的有效数学工具。为了研究π演算的理论性质和应用价值，π演算变体的研究一度成为研究的热点。多类π演算变体应运而生，其研究结果也已经遍及行为等价关系、表达能力、证明系统、程序语言、系统分析和验证等诸多方面。但仍有一些变体未引起足够重视，还有待深入研究。本文主要关注基于名的使用方法的子演算变体、基于传输元组的扩展变体、基于空间敏感语义的扩展变体等三类变体，从观测理论、表达能力和证明系统等三个方面展开研究，主要贡献如下：1.基于名的使用方法的子演算变体。本文在模型独立的交互理论框架下对该类子演算变体进行系统研究。首先定义与绝对等价一致的外部互模拟刻画，并给出绝对等价在有限项上可靠完备的等式证明系统；接着基于子互模拟标准证明π演算和该类变体的表达能力分离结果，并证明绝对等价关系是该类变体自翻译的最大子互模拟关系；然后通过编码可计算模型，证明它们都是交互完备的。2.基于传输元组的扩展变体。本文采用将开项相等的证明转换为进程相等的方法，给出k元π演算有限项上弱互模拟的可靠完备的等式证明系统，弥补多元π演算在证明系统研究方面的不足，并为基于空间敏感语义π变体等价关系的判定方法的研究作铺垫。3.基于空间敏感语义的扩展变体。本文以k元π演算为载体，定义了两种支持通信的空间敏感语义(local cause语义和location语义)变体。基于操作一致性原则，给出这两种变体到k+1元π演算的完全抽象解释，将空间敏感语义互模拟规约到弱互模拟。这些完全抽象解释不仅给出空间敏感语义在交错框架下的刻画，更保持了有限项上的对应关系，从而得到两种空间敏感语义互模拟在有限项上的完备的证明系统，为有限项上真并发语义互模拟的判定方法研究提供新思路。