高階進程演算的互模擬理論和公理化的研究.pdf

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

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

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

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

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

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

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

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

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