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.
Behavioural theory for mobile ambients
MERRO, Massimo;
2004-01-01
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.
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
