RPO semantics for Mobile Ambients

The paper focuses on the synthesis of labelled transition systems (LTSs) for process calculi, choosing as testbed Mobile Ambients (MAs). The proposal is based on a graphical encoding: a process is mapped into a graph equipped with interfaces, such that the denotation is fully abstract with respect to the standard structural congruence. Graphs with interfaces are amenable to the synthesis mechanism based on borrowed contexts (BCs), an instance of relative pushouts (RPOs). The BC mechanism allows the effective construction of an LTS that has graphs with interfaces as states and labels, and such that the associated bisimilarity is a congruence. Our paper focuses on the analysis of an LTS over processes as graphs with interfaces: we use the LTS on graphs to recover an LTS directly defined over the structure of MAs processes, further defining a set of SOS inference rules capturing the same operational semantics.