传名演算变体的互模拟理论,表达能力和证明系统研究
On the Bisimualtion Theory, Expressiveness and Proof System of Some Name-passing Calculi
移动系统无处不在.传名演算,通常称为π演算,是由Milner、Parrow和Walker为了刻画移动系统提出的并发移动模型.π演算不仅是移动系统的基础模型之一,更是描述、分析系统和验证系统正确性的有效数学工具.为了研究π演算的理论性质和应用价值,π演算变体的研究一度成为研究的热点.多类π演算变体应运而生,其研究结果也已经遍及行为等价关系、表达能力、证明系统、程序语言、系统分析和验证等诸多方面.但仍有一些变体未引起足够重视,还有待深入研究.本文主要关注基于名的使用方法的子演算变体、基于传输元组的扩展变体、基于空间敏感语义的扩展变体等三类变体,从观测理论、表达能力和证明系统等三个方面展开研究,主要贡献如下:1.基于名的使用方法的子演算变体.本文在模型独立的交互理论框架下对该类子演算变体进行系统研究.首先定义与绝对等价一致的外部互模拟刻画,并给出绝对等价在有限项上可靠完备的等式证明系统;接着基于子互模拟标准证明π演算和该类变体的表达能力分离结果,并证明绝对等价关系是该类变体自翻译的最大子互模拟关系;然后通过编码可计算模型,证明它们都是交互完备的.2.基于传输元组的扩展变体.本文采用将开项相等的证明转换为进程相等的方法,给出k元π演算有限项上弱互模拟的可靠完备的等式证明系统,弥补多元π演算在证明系统研究方面的不足,并为基于空间敏感语义π变体等价关系的判定方法的研究作铺垫.3.基于空间敏感语义的扩展变体.本文以k元π演算为载体,定义了两种支持通信的空间敏感语义(local cause语义和location语义)变体.基于操作一致性原则,给出这两种变体到k+1元π演算的完全抽象解释,将空间敏感语义互模拟规约到弱互模拟.这些完全抽象解释不仅给出空间敏感语义在交错框架下的刻画,更保持了有限项上的对应关系,从而得到两种空间敏感语义互模拟在有限项上的完备的证明系统,为有限项上真并发语义互模拟的判定方法研究提供新思路.
- 作者：
- 薛建新
- 学位授予单位：
- 上海交通大学
- 专业名称：
- 计算机软件与理论
- 授予学位：
- 博士
- 学位年度：
- 2013年
- 导师姓名：
- 傅育熙
- 中图分类号：
- TP391.1
- 关键词：
- 并发理论；π演算；互模拟；表达能力；证明系统
- Concurrency theory；Pi calculus；Bisimulation；Expressiveness；Proof sys-tem
- 基金项目：
- 国家自然科学%上海市自然科学