Behavioral theory for mobile ambients
Massimo Merro, Francesco Zappa Nardelli · Journal of the ACM · 2005
We study a behavioral theory of 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 which shows that only parallel and nesting contexts need be examined to recover this congruence. (2) We characterize this congruence using a labeled 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.