A Concurrent Graph Semantics for Mobile Ambients1 1Research partly supported by the EC TMR Network General Theory of Graph Transformation Systems (GETGRATS); by the EC Esprit WG Applications of Graph Transformations (APPLIGRAPH); and by the Italian MURST Project Teoria della Concorrenza, Linguaggi di Ordine Superiore e Strutture di Tipi (TOSCA).
Fabio Gadducci, Ugo Montanari · Electronic Notes in Theoretical Computer Science · 2001
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.