【作者】 朱涵；

【导师】 傅育熙；

【作者基本信息】 上海交通大学 ， 计算机软件与理论， 2009， 博士

【摘要】 并发计算是本质上不同于顺序计算的客观现象。许多并发计算模型相继被提出,试图能够像经典计算模型刻画顺序计算那样刻画并发计算。但是这些模型在许多方面缺乏统一的共识,比如基本运算符、操作语义、等价关系等等。这给并发计算的研究带来许多不便,特别是在程序等价、表达能力、图灵完备等领域,而这些又都是最基本的问题。进程演算是一类并发计算模型的统称。它们的共同特点是以通信为基础,使用交错式并发语义等。前面所提到的问题在进程演算中尤为明显,具体表现为许多不同但又相似的演算模型,繁多的等价关系以及不一致的表达能力比较结果等。交互理论正是为了给进程演算一个统一的框架而提出的。它把交互作为最基本的概念,在此基础上定义其他概念。本文的主要工作是在交互理论下重新研究了移动演算中的传名演算。作为交互理论的一个实例,我们重新研究了π演算,重点考察了其上模型独立的等价关系和证明系统。我们还在公平灰箱演算中引入测试等价,并考察了它的一些性质。具体说来,本文从如下几个方面得到了一系列有关交互理论和模型独立观测理论的成果和创新:?π演算上的观测理论研究本文把传名演算的代表π演算在交互理论下进行再研究,主要是考察了其上的各种模型独立等价关系,包括引入新的测试等价。根据交互理论,进程行为的等价性判断应该是只能靠环境与其的交互,也就是环境对进程的观测来达到的。因而对于等价关系的研究我们称为观测理论,绝对等价在π演算中的形式也称为观测等价。我们的π演算将名区分为(常量)名和名变量。操作语义和等价关系的定义则遵照了交互理论的基本原则。这个新模型的表达能力不弱于原来的π演算,但是有着更加漂亮的理论结果和更好的实际应用价值。本文论证了在原来的π演算上的不同等价关系(barbed互模拟、标号互模拟、开互模拟、准开互模拟)都等同于由交互理论基本原则出发定义的观测互模拟。于是我们得到一个更一致的π演算,并且它的理论被大大简化。测试等价也以一种略有不同但更符合交互理论的形式被引入,它严格包含观测等价,符合直观,有着更好的性质。?证明系统的研究公理系统的研究始终是伴随着进程演算发展的。正因为等式公理给出了有关进程等价的代数规则,故进程演算又被称为进程代数。在本文中,研究对象称为证明系统而不是公理系统,是因为本文不是对某一等价关系进行公理化,得出一套等式公理,而是借公理系统的研究得到一套能够证明两个进程相等的系统推理方法。我们将在我们的π演算上,对观测等价和测试等价在有限进程上的证明系统进行考察。为了方便公理化,我们在π演算上引入了选择操作子,但这样会导致观测等价不同余,因为观测等价不在选择操作子下封闭。但是我们发现了P与Q观测等价当且仅当τ.P和τ.Q在公理系统中可证相等,这就给我们提供了一套观测等价的证明方法。我们对测试等价作了相似的研究,也得到了一套证明系统。本文还就有限控制进程的测试等价作了考察。通过进程方程组的刻画,同样给出了有限控制进程上的测试等价的证明系统。?在公平灰箱演算上引入测试等价公平灰箱演算(Fair Ambient,简称FA)是灰箱演算家族的成员之一。它通过在原有的移动灰箱演算(MobileAmbient)中加入补名,加强了对灰箱移入移出的控制。曾经有人研究过灰箱演算上的上下文等价,这是may测试等价的变体,是一种比较弱的等价关系。本文中定义的测试等价充分利用了补名的作用,也就是充分利用交互的性质,使得一部分特殊形式的测试者拥有所有测试者的区分能力。它在有限进程上是一个同余关系,在一类后继终止的进程上严格包含互模拟等价。本文还考察了两种不同的对成功状态的定义,一种是从结构的观点,另一种是从交互的观点。这两种定义得到的是相同的测试等价,这在某种程度上表明了交互理论的合理性。本文还就从π到FA的翻译在测试等价的意义下是否完全抽象作了研究,结果表明这个翻译仍然保持完全抽象。这为π演算是公平灰箱演算的一个子演算的观点增加了重要砝码。本文对交互理论下的模型独立移动演算理论的所得到的研究成果,能够帮助人们深入理解交互理论。我们的π演算可以认为是在交互理论下重新认识进程演算的第一个实例,而对等价关系的研究表明进程演算中的等价关系能够统一到一个更加客观,独立于模型的关系。对于box等价的研究也显示出原本出发点很不相同的测试理论可以被很好地纳入交互理论。这些为进一步用交互理论研究进程演算、研究并发计算提供了非常有意义的尝试。更多还原

【Abstract】 Concurrent computation is inherently different to sequential compu-tation. In the literature, researchers have proposed many concurrent mod-els in an effort to capture concurrent computation, trying to be as suc-cessful as classical computation models in capturing sequential computa-tion. However, these concurrent models lack some fundamental commonground, like basic operators, operational semantics and equivalence rela-tions. Consequently, it has many negative effects on the research of con-current computation, especially on program equality, expressiveness andTuring completeness, the most fundamental parts of concurrency theory.Process calculi are mathematical models for describing and analysingproperties of concurrent computation with some characteristics in com-mon. These common points include the facts that they are based uponcommunication, that they are using interleaving semantics, etc. The neg-ative effects mentioned above affect process calculi even more apparently.We have a plethoral of similar but different calculi, many incompatibleequivalence relations, and chaotic results on expressiveness.The theory of interaction of Fu has been proposed to give processcalculi a unified framework. It features interaction as the most basic prim-itive, upon which other concepts are build. The main contributions of thisthesis are investigations of model independent thoery of mobile calculiunder this framework. As a paradigm of the theory of interaction, we re-visit theπ-calculus of name-passing calculi, and compare the well-knownequivalence relations and proof systems on it. We also introduce testingequivalence into the Calculus of Fair Ambients. The contributions of the thesis can be summarized as follows:? Investigationsoftheobservationaltheoryareconductedonπ-calculus.We revisit theπ-calculus in the theory of interaction. Equalities onπ-calculus are investigated. These equalities include testing equiva-lence. Ourπ-calculus has disjoint sets of names and name variables.Its operational semantics and equivalence relation are redefined, ad-hering to the principles of the theory of interaction. The advantageof the new formulation is that it enjoys a simpler theory and is closerto computing practice. In this thesis, it is showed that many equiv-alence relations on the originalπ-calculus (barbed bisimilarity, la-belled bisimilarity, open bisimilarity, quasi-open bisimilarity) coin-cide with the observational bisimilarity, which is defined upon theprinciples of the theory of interaction. We have a more consistentπ-calculus with simplified theory. Testing equivalence is also intro-duced to theπ-calculus in a slightly different form.? Proof systems of the observational equality and testing equivalenceare established.Axiomatization is a crucial part of the research on process calculi.Because axioms provide us with algebraic rules about equivalencerelations, process calculi are also known as process algebra. In thisthesis we are concerning ourselves about proof systems rather thanaxiom systems. We are not axiomatizing particular equivalence re-lations, instead we construct systems which can prove whether twoprocesses are equivalent. In order to faciliate axiomatisation, we in-troduce unguarded choice. It breaks the congruence of observationalequality. We observe that P equals to Q if and only ifτ.P andτ.Qare provably equal in this system. This gives us a general method todecide whether two processes are observationally equal. A similartreatment is given to testing equivalence, for which we also obtain aproof system. We also investigate finite controlπ-processes. We give a proof system for box equivalence on finite controlπ-processes.? Testing equivalence is defined and investigated for the Calculus ofFair Ambient.The Calculus of Fair Ambient (FA for short) adds co-names to theCalculus of Mobile Ambient in order to strengthen the control ofambient movements. A variant of may testing equivalence, contex-tual equivalence, has been proposed for the Calculus Mobile Am-bient. But it is very weak. The testing equivalence defined in thisthesis exploits the functions of conames, making full use of inter-action. It is showed that the observers in some special form havethe full discriminating power that all observers have. It is a con-gruence on finite processes. On hereditarily terminating processesit strictly contains bisimilarity. It is also proved in this thesis thattwo definitions of successful states, one from a structural viewpointand another from an interactive viewpoint, result in the same testingequivalence relation. This justifies the theory of interaction to someextent. This thesis also investigates the encoding fromπ-calculus toFA, showing that it is also fully abstract with respect to the testingequivalence. This adds weights to the viewpoint thatπ-calculus is asubcalculus of FA.The results in this thesis give us a deeper insight into both the theoryof interaction and name-passing calculi. ourπ-calculus can be consid-ered as a paradigm of redefining process calculi in the theory of interac-tion. The coincidence theory in this thesis tells that equivalence relationscan be unified to a single, objective and model independent relation. Boxequivalence also shows that testing equivalence, which is originally de-fined in a different style, can be integrated into the theory of interactionsmoothly. All theses results are of significance in reinforcing the view thatprocess calculi and concurrent computation should be investigated in asingle framework.更多还原