Behavioural Theory for Mobile Ambients

Abstract : We study a behavioural theory of Cardelli and Gordon's Mobile Ambients, a process calculus for modelling mobile agents in wide-area networks, focussing on reduction barbed congruence. Our contribution is threefold. We prove a context lemma that shows that only parallel and nesting contexts need be examined to recover this congruence. We characterise this congruence using a labelled bisimilarity: this requires novel techniques to deal with asynchronous movements of agents and with the invisibility of migrations of secret locations. We develop refined proof methods involving up-to proof techniques, which allow us to verify a set of algebraic laws and the correctness of more complex examples.
Document type :
Reports
Complete list of metadatas

Cited literature [43 references]  Display  Hide  Download

https://hal.inria.fr/inria-00070628
Contributor : Rapport de Recherche Inria <>
Submitted on : Friday, May 19, 2006 - 9:03:04 PM
Last modification on : Friday, May 25, 2018 - 12:02:03 PM
Long-term archiving on : Monday, September 17, 2012 - 4:01:01 PM

Identifiers

  • HAL Id : inria-00070628, version 1

Collections

Citation

Massimo Merro, Francesco Zappa Nardelli. Behavioural Theory for Mobile Ambients. [Research Report] RR-5375, INRIA. 2004, pp.61. ⟨inria-00070628⟩

Share

Metrics

Record views

171

Files downloads

264