Behavioural theory for mobile ambients

Abstract

We study the behavioural theory of Cardelli and Gordon's Mobile Ambients, by focusing on a standard contextual equivalence, reduction barbed congruence. We prove a context lemma that allows the derivation of contextual equivalences by considering only contexts for concurrency and locality. We go further and give a characterisation of reduction barbed congruence over arbitrary processes in terms of a labelled bisimilarity defined over a restricted class of processes, called systems. This characterisation extends and completes an earlier result on bisimulation proof methods for Mobile Ambients, that was restricted to systems. The characterisation is then used to prove a collection of algebraic laws. © 2004 Springer Science + Business Media, Inc.