傳名演算變體的互模擬理論,表達能力和證明系統(tǒng)研究.pdf

1、移動系統(tǒng)無處不在。傳名演算，通常稱為π演算，是由Milner、Parrow和Walker為了刻畫移動系統(tǒng)提出的并發(fā)移動模型。π演算不僅是移動系統(tǒng)的基礎模型之一，更是描述、分析系統(tǒng)和驗證系統(tǒng)正確性的有效數(shù)學工具。為了研究π演算的理論性質(zhì)和應用價值，π演算變體的研究一度成為研究的熱點。多類π演算變體應運而生，其研究結(jié)果也已經(jīng)遍及行為等價關系、表達能力、證明系統(tǒng)、程序語言、系統(tǒng)分析和驗證等諸多方面。但仍有一些變體未引起足夠重視，還有待深入研究

2、。
　　 本文主要關注基于名的使用方法的子演算變體、基于傳輸元組的擴展變體、基于空間敏感語義的擴展變體等三類變體，從觀測理論、表達能力和證明系統(tǒng)等三個方面展開研究，主要貢獻如下:
　　 1.基于名的使用方法的子演算變體。本文在模型獨立的交互理論框架下對該類子演算變體進行系統(tǒng)研究。首先定義與絕對等價一致的外部互模擬刻畫，并給出絕對等價在有限項上可靠完備的等式證明系統(tǒng);接著基于子互模擬標準證明π演算和該類變體的表達能力分離結(jié)

3、果，并證明絕對等價關系是該類變體自翻譯的最大子互模擬關系;然后通過編碼可計算模型，證明它們都是交互完備的。
　　 2.基于傳輸元組的擴展變體。本文采用將開項相等的證明轉(zhuǎn)換為進程相等的方法，給出k元π演算有限項上弱互模擬的可靠完備的等式證明系統(tǒng)，彌補多元π演算在證明系統(tǒng)研究方面的不足，并為基于空間敏感語義π變體等價關系的判定方法的研究作鋪墊。
　　 3.基于空間敏感語義的擴展變體。本文以k元π演算為載體，定義了兩種支持通信