CCS的基本問(wèn)題研究.pdf

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

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

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

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

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

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

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

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