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

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.
1402081405
Mobile Computing; Operational semantics; Behavioural Theory
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11562/20881
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 2
  • ???jsp.display-item.citation.isi??? 1
social impact