CCS的基本問題研究.pdf

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

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

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

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

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

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

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

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