A decentralised graphical implementation of mobile ambients

摘要

We present a graphical implementation for finite processes of the mobile ambients calculus. Our encoding uses unstructured (i.e., non-hierarchical) graphs and it is sound and complete with respect to the structural congruence of the calculus (i.e., two processes are equivalent iff mapped to isomorphic graphs). With respect to alternative proposals for the graphical implementation of mobile ambients, our encoding distinguishes the syntactic structure of a process from the activation order of its components. Our solution faithfully captures a basic feature of the calculus (ambients can be nested and reductions are propagated across the nesting) and it allows to model the reduction semantics via a graph transformation system containing just three rules.