CCS的基本問題研究.pdf

1、CCS(A Calculus of Communicating System)是由R.Milner在1980年提出的用以描述并發(fā)交互系統(tǒng)的抽象計算模型?，F(xiàn)代最著名的并發(fā)計算模型，包括傳值演算、傳名演算和高階演算等都可以視為CCS的擴(kuò)展。區(qū)別于傳統(tǒng)計算模型如λ-演算和Turing機(jī)，CCS將通信（或同步）作為基本概念，又將復(fù)合(composition)算子和局部化(localization)算子作為表達(dá)系統(tǒng)交互的基本語法構(gòu)造子。復(fù)合算子使

2、系統(tǒng)得到交互能力，局部化算子使系統(tǒng)失去交互能力。
　　寫作本文恰逢CCS誕生三十年。在過去的三十年里，進(jìn)程演算在理論和應(yīng)用上得到了高度發(fā)展。盡管如此，仍然存在相當(dāng)一部分基本問題在文獻(xiàn)中缺少深入地討論，其中的一些問題甚少有人提及，另一些問題人們的認(rèn)識尚比較模糊。
　　本文在對已有工作認(rèn)真理解和總結(jié)的基礎(chǔ)上，對CCS這一經(jīng)典語言用新的方式進(jìn)行闡述。我們將注意力集中在以下三個方面:
　　1.進(jìn)程的觀察理論(Observati

3、onal Theory)。進(jìn)程理論中的基本問題是什么時候兩個系統(tǒng)可以看作是相等的;以及什么時候一個系統(tǒng)可以看作是另一個系統(tǒng)的近似。觀察理論就要解決這個問題。文獻(xiàn)中一般采用的方法是先對進(jìn)程模型建立標(biāo)號遷移系統(tǒng)(labelled transition system)，然后在標(biāo)號遷移系統(tǒng)上定義等價或前序關(guān)系。這種做法的缺點是等價或前序關(guān)系的定義依賴于具體的模型。如果模型作了改變，其中一些關(guān)系有可能不再有意義，另一些關(guān)系可能需要重新定義以適應(yīng)于

4、新的模型。
　　本文對觀察理論的研究將采取完全不同的途徑。首先，我們從已有的進(jìn)程觀察等價或前序關(guān)系中提煉出一些基本性質(zhì)，如可擴(kuò)展性(extensionality)、交互能力的等勢性(equipollence)(或保持性(preservation))。然后，進(jìn)程行為等價或前序?qū)⒂蛇@些性質(zhì)直接定義。這樣做確保了等價或前序關(guān)系的定義是模型無關(guān)的。而對于具體的模型，可以進(jìn)一步找出這些模型無關(guān)定義所對應(yīng)的操作刻畫，即模型有關(guān)的描述。具體說來

5、，本文將基于對環(huán)境的不同假設(shè)，提出一系列模型無關(guān)的觀察等價和前序關(guān)系;討論這些關(guān)系之間的相互聯(lián)系;定義和研究常見的行為性質(zhì);找出了這些關(guān)系在CCS下對應(yīng)的操作刻畫。在此研究過程中，我們發(fā)現(xiàn)了一些新的進(jìn)程前序關(guān)系，并指出文獻(xiàn)中的某些關(guān)系并不存在模型無關(guān)的定義。
　　2.CCS的表達(dá)能力(Expressiveness)。在程序語言理論中，研究不同語言之間的相對表達(dá)能力的有效工具是翻譯。但如何評判翻譯的好壞并沒有統(tǒng)一的說法。對于交互模型

6、之間翻譯的評判標(biāo)準(zhǔn)，人們的認(rèn)識也并不十分清楚。在大多數(shù)文獻(xiàn)中給出的翻譯，其作者也僅僅強(qiáng)調(diào)所謂的完全抽象性(fullabstraction)。這一術(shù)語或概念來源于指稱語義，其弊端是它不反映模型間的操作對應(yīng)關(guān)系。對于聯(lián)系緊密的模型而言，完全抽象性質(zhì)顯得過于粗糙。另外一些標(biāo)準(zhǔn)，比如說同態(tài)，實際上是將代數(shù)性質(zhì)和觀察性質(zhì)混淆了起來，從而是不必要的。傅最近提出的subbisimilarity標(biāo)準(zhǔn)對進(jìn)程模型間翻譯標(biāo)準(zhǔn)的進(jìn)一步認(rèn)識作了深入探索。

7、　　本文研究CCS各子語言間的相對表達(dá)能力，著眼于不同的子語言之間翻譯的存在性問題。文中采用的評判標(biāo)準(zhǔn)是之前定義的模型無關(guān)的進(jìn)程等價關(guān)系的衍生，這可以看作是subbisimilarity標(biāo)準(zhǔn)的簡易版本。由于本文會定義一系列進(jìn)程等價關(guān)系，從而也就有必要考察一系列翻譯的評判標(biāo)準(zhǔn)，相應(yīng)結(jié)論也會由于標(biāo)準(zhǔn)不同而變化。此外，文章還考察了CCS的Turing完備性以及它與局部名操縱能力之間的聯(lián)系。
　　3.CCS上雙模擬等價和模擬前序的驗證問題

8、(Verification Problems)。進(jìn)程等價驗證的算法研究是極其重要的方向，但是涉及CCS的非平凡子演算的研究結(jié)果很少。主要原因是過去對CCS的子演算沒有比較好的分層。本文根據(jù)局部名的操縱能力從弱到強(qiáng)把CCS分成四類:不含局部名、只含有靜態(tài)局部名、只含有不能移動局部名、含有允許移動的局部名。我們用“防御者脅迫(Defender's Forcing)”方法證明了即使只含有靜態(tài)局部名，CCS的強(qiáng)雙模擬等價也不可判定。通過對Min