Bisimulation Proof Methods for Mobile Ambients

We study the behavioural theory of Cardelli and Gordon’s Mobile Ambients. We give an lts based operational semantics, and a labelled bisimulation based equivalence that coincides with reduction barbed congruence. We also provide two up-to proof techniques that we use to prove a set of algebraic laws, including the perfect firewall equation.

• Type: Conference
• Year: 2003
• Where: ICALP
• Authors: Massimo Merro, Francesco Zappa Nardelli
• Keywords: Bisimulation Based Equivalence, Gordon’s Mobile Ambients, ICALP 2003, Reduction Barbed Congruence, Theoretical Computer Science