鲁棒环境演算中的互模拟同余关系  

Bisimulation Congruence in Robust Ambient Calculus

作　　者：陈韬略[1] 李斌[1] 韩婷婷[1] 吕建[1] 

机构地区：[1]南京大学计算机软件新技术国家重点实验室,南京210093

出　　处：《南京大学学报（自然科学版）》2005年第2期155-161,共7页Journal of Nanjing University（Natural Science）

基　　金：国家重点基础研究发展规划973项目(2002CB312002);国家自然科学基金(60273034;60233010;60403014);国家863高科技项目(2002AA116010);江苏省自然科学基金(BK2002203;BK2002409)

摘　　要：　移动计算是在网络技术发展过程中涌现出来的一种新的分布计算范型,移动环境演算是一种广为使用的描述移动计算的形式化模型.针对这种演算的一种改进———鲁棒环境演算,提出了一个新的标号转移系统,并在此基础上引进了一种互模拟同余关系.同时,作为上述工作的应用,给出了一些重要进程等价性定律的简洁证明.Computation with mobility has been a novel distributed computation paradigm with the development of network technology. The calculus of Mobile Ambient is a widely studied formal mechanism for describing both mobile computing and mobile computation. This paper deals with the algebra theory of a variant of this calculus, the Robust Mobile Ambient. The traditional semantics for this calculus is usually defined on the basis of reduction semantics and thus the process equivalences are generally given in the style of testing or barbed bisimulation, which makes the reasoning and verification of such equivalences notoriously difficult. This paper aims to provide some approaches to remedy these problems. In detail, by introducing the notion of prefix, action and concretion, this paper provides a new labelled transition system as the semantics of the calculus. It is shown that the new semantics coincides with the traditional reduction-based semantics. Based on it, this paper introduces a novel bisimulation relation. The main advantages of this new relation lie in that it is a congruence relation and the co-inductive proof techniques can be applied which can alleviate the difficulties of proof for process equivalences greatly. At the same time, the new relation enjoys intuition soundness. As the application of above work, this paper also presents concise proofs for some important process equivalence laws.

关 键 词：进程代数 环境演算 标号转移系统 互模拟 

分 类 号：TP301.6[自动化与计算机技术—计算机系统结构]