[moca] Paper Announcement: Behavioural Theory for Mobile Ambients

["Massimo Merro" <merro@xxxxxxxxxxxx>]

We would like to announce the following INRIA Technical Report on the
the Behavioural Theory of Mobile Ambients. Part of the material of the
TR has already appeared in the proceedings of ICALP'03 and IFIP TCS'04.
The TR can be downloaded at

                       http://www.inria.fr/rrrt/rr-5375.html

We will be very glad to hear any comments.

Best,

Massimo Merro
Francesco Zappa Nardelli.

-----------------------------------------------------------------------
-----------------------------------------------------------------------

Title:  Behavioural Theory for Mobile Ambients

Authors: Massimo Merro and Francesco Zappa Nardelli

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.
(1) We prove a context lemma that shows that only parallel and nesting
contexts need be examined to recover this congruence. (2) 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. (3) 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.



  
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The "models for mobility" mailing list     mailto:moca@xxxxxxxxxxxxxxx
 http://www-sop.inria.fr/mimosa/personnel/Davide.Sangiorgi/moca.html