CCS(A Calculus of Communicating System)是由R.Milner在1980年提出的用以描述并发交互系统的抽象计算模型。现代最著名的并发计算模型,包括传值演算、传名演算和高阶演算等都可以视为CCS的扩展。区别于传统计算模型如λ-演算和Turing机,CCS将通信(或同步)作为基本概念,又将复合(composition)算子和局部化(localization)算子作为表达系统交互的基本语法构造子。复合算子使系统得到交互能力,局部化算子使系统失去交互能力。写作本文恰逢CCS诞生三十年。在过去的三十年里,进程演算在理论和应用上得到了高度发展。尽管如此,仍然存在相当一部分基本问题在文献中缺少深入地讨论,其中的一些问题甚少有人提及,另一些问题人们的认识尚比较模糊。本文在对已有工作认真理解和总结的基础上,对CCS这一经典语言用新的方式进行阐述。我们将注意力集中在以下三个方面:1.进程的观察理论(Observational Theory)。进程理论中的基本问题是什么时候两个系统可以看作是相等的;以及什么时候一个系统可以看作是另一个系统的近似。观察理论就要解决这个问题。文献中一般采用的方法是先对进程模型建立标号迁移系统(labelled transition system),然后在标号迁移系统上定义等价或前序关系。这种做法的缺点是等价或前序关系的定义依赖于具体的模型。如果模型作了改变,其中一些关系有可能不再有意义,另一些关系可能需要重新定义以适应于新的模型。本文对观察理论的研究将采取完全不同的途径。首先,我们从已有的进程观察等价或前序关系中提炼出一些基本性质,如可扩展性(extensionality)、交互能力的等势性(equipollence)(或保持性(preservation))。然后,进程行为等价或前序将由这些性质直接定义。这样做确保了等价或前序关系的定义是模型无关的。而对于具体的模型,可以进一步找出这些模型无关定义所对应的操作刻画,即模型有关的描述。具体说来,本文将基于对环境的不同假设,提出一系列模型无关的观察等价和前序关系;讨论这些关系之间的相互联系;定义和研究常见的行为性质;找出了这些关系在CCS下对应的操作刻画。在此研究过程中,我们发现了一些新的进程前序关系,并指出文献中的某些关系并不存在模型无关的定义。2. CCS的表达能力(Expressiveness)。在程序语言理论中,研究不同语言之间的相对表达能力的有效工具是翻译。但如何评判翻译的好坏并没有统一的说法。对于交互模型之间翻译的评判标准,人们的认识也并不十分清楚。在大多数文献中给出的翻译,其作者也仅仅强调所谓的完全抽象性(full abstraction)。这一术语或概念来源于指称语义,其弊端是它不反映模型间的操作对应关系。对于联系紧密的模型而言,完全抽象性质显得过于粗糙。另外一些标准,比如说同态,实际上是将代数性质和观察性质混淆了起来,从而是不必要的。傅最近提出的subbisimilarity标准对进程模型间翻译标准的进一步认识作了深入探索。本文研究CCS各子语言间的相对表达能力,着眼于不同的子语言之间翻译的存在性问题。文中采用的评判标准是之前定义的模型无关的进程等价关系的衍生,这可以看作是subbisimilarity标准的简易版本。由于本文会定义一系列进程等价关系,从而也就有必要考察一系列翻译的评判标准,相应结论也会由于标准不同而变化。此外,文章还考察了CCS的Turing完备性以及它与局部名操纵能力之间的联系。3. CCS上双模拟等价和模拟前序的验证问题(Verification Problems)。进程等价验证的算法研究是极其重要的方向,但是涉及CCS的非平凡子演算的研究结果很少。主要原因是过去对CCS的子演算没有比较好的分层。本文根据局部名的操纵能力从弱到强把CCS分成四类:不含局部名、只含有静态局部名、只含有不能移动局部名、含有允许移动的局部名。我们用“防御者胁迫(Defender’s Forcing)”方法证明了即使只含有静态局部名,CCS的强双模拟等价也不可判定。通过对Minsky机器“不确定”的翻译证明即使局部名不能移动,CCSCCS与有限状态进程的双模拟等价和两侧的模拟前序都可判定。借助于结构膨胀序(Structural Expansion Order),利用“双模拟基(Bisimulation Base)”和“扩张树(Expansion Tree)”技术,证明如果局部名不允许移动,那么有限状态进程到CCS的单侧模拟前序可判定。这些结论从另一个侧面反映出局部名的移动能力对进程的相对表达能力的影响。