A concurrent graph semantics for Mobile Ambients

We present an encoding for finite processes of the mobile ambients calculus into term graphs, proving its soundness and completeness with respect to the original, interleaving operational semantics. With respect to most of the other approaches for the graphical implementation of calculi with name mobility, our term graphs are unstructured (that is, non hierarchical), thus avoiding any "encapsulation" of processes. The implication is twofold. First of all, it allows for the reuse of standard graph rewriting theory and tools for simulating the reduction semantics. More importantly, it allows for the simultaneous execution of independent reductions, which are nested inside ambients, thus offering a concurrent semantics for the calculus