Recent years have seen an increasing use of graphical formalisms for modelling concurrent and distributed systems.
Among other proposals, many authors discussed graphical presentations for process calculi, where graphs model processes and (ad hoc or standard) graph rewriting techniques are used to simulate the reduction semantics of the calculus at hand.
One of the advantages of using graphs is the elimination of problems concerning the implementation of reductions over the structural congruence, such as the α-conversion of bound names. Moreover, the use of standard graph trasformation mechanisms, such as the double-pushout approach, to model the reduction semantics of the calculus, allows us to exploit the well-established concurrent semantics for graph rewriting.
Graphical encoding mapping processes into graphs equipped with suitable interfaces can be also used to distill labelled transition systems (LTSs) on (processes encoded as) graphs, by applying the borrowed context (BC) mechanism, wich is an instance of the theory of reactive systems, introduced by Leifer and Milner.
We proposed a graphical encoding for mobile ambients (MAs) and we captured
the reduction semantics by a set of graph transformation rules. Then, we used the encoding to distill a LTS on (processes encoded as) graphs, by applying BC mechanism and we exploited it to recover a suitable LTS directly defined over the structure of MAs processes. Finally, we proved that the resulting LTS is the same as the one previously proposed by Rathke and Sobocinski.
However, as it is typical for reactive systems, the bisimilarity on the derived LTS is resulted to be too strict. Indeed, the most important drawbacks reactive systems suffer from, concerns the inadequacy of the abstract semantics induced by the derived LTS.
We tackled this problem by proposing the notions of strong and weak barbed saturated semantics for reactive systems. We instantiated the framework over MAs, proving that it can capture the strong and the weak reduction barbed congruence for MAs, proposed by Rathke and Sobocinski and by Merro and Zappa Nardelli, respectively.