非对称性和不等名算子下的Barbed同余关系
Barbed Congruence of Asymmetry and Mismatch
-
摘要: 进程代数的研究目的是在代数框架内研究并发系统的模型。其中,对进程代数的发展起到重大影响的有CCS演算、pi演算等。Chi演算是在pi演算的基础上发展而来的。本文在chi演算框架下研究了非对称通信和不等名算子之间的相互影响。之所以着重考虑这两个结构,是基于如下原因:(1)Chi演算的一个显著特点是,具有对称的通信规则。就理论研究而言,通信的对称性是一个完美的性质。但是由于对称性会引入额外的不确定性,而这是用户所不希望看到的,因此在实际编程中往往需要非对称的通信方式。因此,我们有必要像关注对称chi演算那样关注非对称chi演算。已有研究结果表明,非对称chi演算的代数理论比对称chi演算要丰富得多。(2)二元指令if B then C1 else C2是一个常见的编程结构。在移动进程计算中,该指令可以编码为进程x=yP + x≠yQ,因此不等名条件在这里起到了关键的作用。实际上,即便是用两个连续的一元指令if B then C1; if ?B then C2去模拟该指令,第二条指令中所出现的否定算子也预示着,要把这段代码翻译为某个移动进程演算中的进程,不等名条件也是不可缺少的。在许多编程应用中, 如果不计较程序的复杂性,那么只要有等名算子x=y就足够了,但是前提条件是计算流程中只有有限多个名。在无限多个名的情况下,如果不允许不等名算子的存在,而是在演算中扩充其他的结构,如无限和,那么得到的演算将更加抽象。正是为了适应实际需要,不等名算子在理论研究中才显得尤为重要。在chi演算中研究不等名算子得到的结果表明该算子对代数理论的影响是非常微妙的,甚至在定义互模拟的概念时也需要格外注意。由此可见,非对称通信和不等名算子这两个特征结构在实际应用和理论研究中都是非常重要的。通常这两个结构被整合到高级程序结构中,很难分离出来单独研究。Chi演算则为集中研究这两个结构提供了一种可能的框架。由于barbed互模拟关系能够有效地生成一个合理的观察等价关系,具有一定的普适性,并得到了广泛的研究,因此本文主要研究了在该演算中barbed互模拟关系的操作性质和代数性质,给出了其相应的开形式等价定义,根据该定义可以清楚地了解barbed互模拟进程对的行为方式。在移动计算模型的代数理论研究中,一个非常重要的问题是如何给出进程同余关系的可靠而完备的公理化系统,这样一个完备的推理系统不仅对于深刻理解同余关系是至关重要的,而且奠定了同余关系自动推理的理论基础。本文在开barbed互模拟的基础上定义了barbed同余关系,并为其建立了可靠而完备的等式公理系统。本文的研究结果有助于更深入地理解该演算的互模拟行为,并基本上描绘出了两种结构对移动进程观察理论的影响。Abstract: The \chi calculus is a model of concurrent and mobile systems. Itemphasizes that communications are information exchanges. In the paper,two constructions are incorporated into the framework of the chicalculus, which are asymmetric communication and mismatch conditionwidely used in applications. Since the barbed bisimilarity has provedits generality and gained its popularity as an effective approach togenerating a reasonable observational equivalence, we study both theoperational and algebraic properties of the barbed bisimilarity in thisenriched calculus. The investigation supports an improved understandingof the bisimulation behaviors of the model. It also gives a generalpicture of how the two constructions affect the observational theory.