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

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

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

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