高階進(jìn)程演算的互模擬理論和公理化的研究.pdf

1、高階進(jìn)程演算，因?yàn)槠浜軓?qiáng)的抽象能力和理論上的重要性，在進(jìn)程演算領(lǐng)域一直得到廣泛的關(guān)注，并成為描述和分析具有動(dòng)態(tài)變換特性的內(nèi)部連接結(jié)構(gòu)的移動(dòng)系統(tǒng)的有效數(shù)學(xué)工具。在本文中，我們對(duì)高階進(jìn)程演算就如下幾方面進(jìn)行了研究。 ·帶有mismatch的高階π演算：互模擬理論；帶有mismatch的高階π演算的線性片段：公理化。 高階進(jìn)程演算的公理化問(wèn)題，如高階π演算的公理化問(wèn)題，一直以來(lái)鮮有相關(guān)工作。然而無(wú)論在理論上還是在應(yīng)用中，判斷兩

2、個(gè)高階進(jìn)程是否在某種互模擬下等價(jià)都有其重要意義，這中判斷需要一個(gè)能夠有效地進(jìn)行分析并給出結(jié)論的算法。從算法的觀點(diǎn)看，mismatch是在互模擬理論以及公理化中都是很有用的操作子；我們通過(guò)考察帶有mismatch的高階π演算來(lái)深入研究了公理化問(wèn)題。我們首先形式化地定義并討論了存在mismatch時(shí)的互模擬理論，其中我們的互模擬稱為開弱高階互模擬，這是一種non-delayed型的開型互模擬。隨后，在設(shè)計(jì)公理系統(tǒng)時(shí)我們采用了線性方法，即將演

3、算限制到線性片段上。利用對(duì)開弱高階互模擬的刻畫，包括前綴進(jìn)程間等價(jià)與其延續(xù)進(jìn)程間等價(jià)之間的關(guān)系以及線性演算獨(dú)有的性質(zhì)，我們最終證明了公理系統(tǒng)的完備性。 我們對(duì)高階互模擬理論和公理化的研究，不僅通過(guò)引入一個(gè)有用的操作子對(duì)以往的工作進(jìn)行了擴(kuò)展，且將高階公理化的研究又向前推進(jìn)了一步，同時(shí)為對(duì)其它高階演算(如Ambient演算)的研究提供了參考。 ·高階CCS編碼一階π演算。 不同演算之間的編碼是比較它們的表達(dá)能力的有效

4、方法，可以揭示它們之間的本質(zhì)區(qū)別。Thomsen和Sangiorgi對(duì)高階演算(分別是高階CCS和高階π演算)與一階π演算之間的相互編碼進(jìn)行了研究，但他們的工作尚不完整，缺少對(duì)用高階CCS對(duì)一階π演算編碼的全抽象性質(zhì)的深入研究。在本文中，我們?cè)噲D解決這一問(wèn)題。我們基于Thomsen的編碼方法，將一階π演算翻譯到PlainCHOCS中。我們證明這種編碼方法在基互模擬性(一階π演算中)和wired互模擬性(PlainCHOCS中)下是全抽象

5、的，其中wired互模擬性是我們定義的基于僅發(fā)送和接收線纜(wire)的wired進(jìn)程的一種互模擬，它們是編碼策略的核心。進(jìn)一步，由于wired互模擬性蘊(yùn)含廣為人知的上下文互模擬性，我們確保了在基互模擬性和上下文互模擬性下編碼的可靠性。我們使用領(lǐng)域中已有的索引技術(shù)來(lái)處理技術(shù)細(xì)節(jié)中的難點(diǎn)以獲得主要結(jié)論，即將索引技術(shù)應(yīng)用到原始編碼方法中，以此來(lái)處理編碼中產(chǎn)生的額外內(nèi)部動(dòng)作，隨后將帶索引的編碼方法中所獲得的結(jié)果移植得到原始編碼中的相應(yīng)結(jié)論。我

6、們還討論了如何通過(guò)在兩個(gè)演算中選擇合理的互模擬來(lái)獲得全抽象性質(zhì)等問(wèn)題。 我們對(duì)進(jìn)程演算間編碼的研究解決了關(guān)于在高階CCS中表達(dá)一階π演算的一個(gè)未決問(wèn)題，從而補(bǔ)充了這兩類演算之間的編碼研究，這進(jìn)一步展現(xiàn)了一階演算和高階演算之間的關(guān)系。此外，編碼研究的結(jié)果還提供了用高階演算來(lái)實(shí)現(xiàn)對(duì)λ演算編碼的另一種方法。 ·線性高階π演算中局部互模擬的邏輯刻畫。 除了用代數(shù)方法對(duì)高階進(jìn)程演算的互模擬進(jìn)行工作外，從邏輯角度對(duì)互模擬的研

7、究也有其價(jià)值所在，目前已經(jīng)有對(duì)PlainCHOCS中的強(qiáng)和弱上下文互模擬進(jìn)行邏輯刻畫的工作。在本文中，我們用邏輯的方法對(duì)線性進(jìn)程演算進(jìn)行了一些新的研究。我們致力于找到一種對(duì)線性高階π演算中局部互模擬的邏輯刻畫。為此我們通過(guò)兩步來(lái)完成準(zhǔn)備：首先我們通過(guò)一些變體來(lái)簡(jiǎn)化局部互模擬性；其次我們通過(guò)互模擬遞減鏈來(lái)逼近局部互模擬性。為實(shí)現(xiàn)邏輯刻畫，我們對(duì)演算進(jìn)行了重新形式化，以獲得相對(duì)容易實(shí)現(xiàn)刻畫的等價(jià)形式(在互模擬意義上)。我們的邏輯具有完整的非

8、操作(對(duì)偶性)，并且比已有的邏輯語(yǔ)言簡(jiǎn)單，這體現(xiàn)在高階模態(tài)鈹降階為類似于一階模態(tài)，且構(gòu)造蘊(yùn)含操作子僅被用于處理一階受限輸出。我們證明了刻畫定理，它將邏輯等價(jià)與局部互模擬性相關(guān)聯(lián)。 我們關(guān)于邏輯刻畫的丁作對(duì)高階進(jìn)程演算研究的意義在于提供了另一種觀點(diǎn)，即邏輯的觀點(diǎn)，以此補(bǔ)充了代數(shù)角度的研究。此外，將檢驗(yàn)互模擬等價(jià)轉(zhuǎn)換為檢驗(yàn)邏輯等價(jià)使得我們馬上可以使用邏輯的一整套方法，后者不但具有諸多模型檢測(cè)算法，而且有許多實(shí)J{j的工具。

9、本文不僅對(duì)高階進(jìn)程演算領(lǐng)域內(nèi)的幾個(gè)方面的問(wèn)題進(jìn)行了研究，且傳遞了幾點(diǎn)有意義的信息。首先是線性性質(zhì)在確保高階演算的可靠且完備的公理系統(tǒng)中具有重要意義，這-特征成功的降低了通信進(jìn)程的表達(dá)能力。其次，作為用一階π演算來(lái)表達(dá)高階演算的補(bǔ)充，我們證明了其反向在一些合理的互模擬性下亦成立，這使得我們可以更加確信高階演算的相對(duì)獨(dú)立性，結(jié)合其特有的抽象能力，這種獨(dú)立性使得高階演算更有吸引力。再次，通過(guò)展示一種可以刻畫互模擬等價(jià)的簡(jiǎn)單且完備的邏輯語(yǔ)言，我