ABSTRACT

Computation with mobility becomes a novel distributed computation paradigm with the development of network technology. The calculus of Mobile Ambient (MA) 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 (ROAM). Hitherto, for ROAM, the criterion of process equivalence is contextual equivalence, whose main disadvantage lies in that the proof and verification for process equivalence are usually very hard. To remedy this deficiency to some extend, we provide a new labelled transition system, and based on it, a bisimulation relation is introduced as the criterion of behavior equivalence. We justify the soundness of definition by showing that it is a congruence relation and to illustrate the advantage of the new behavior equivalence relation, this paper also gives concise proofs for some important process equivalence laws studied in literature.