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

Bisimulation Congruence in Robust Ambient Calculus

移动计算是在网络技术发展过程中涌现出来的一种新的分布计算范型,移动环境演算是一种广为使用的描述移动计算的形式化模型.针对这种演算的一种改进———鲁棒环境演算,提出了一个新的标号转移系统,并在此基础上引进了一种互模拟同余关系.同时,作为上述工作的应用,给出了一些重要进程等价性定律的简洁证明.

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.