DidaWiki

We discuss some techniques for deriving labelled transition systems (LTSs) and bisimulation congruences for graphical encoding of process calculi. We consider graphical encodings (over graphs equipped with suitable interfaces) such that the structural congruence of processes is captured by graph isomorphism, and the reduction semantics is modeled by a set of graph transformation rules, specified using the DPO approach. These graphs are then amenable to the borrowed contexts (BCs) mechanism, an instance of relative pushouts, which allows the effective construction of a LTS that has minimal graph contexts as labels, and such that the associated bisimilarity is automatically a congruence. However for most calculi the semantics via minimal contexts turns out to be too discriminating, therefore barbed saturated semantics has to be taken into account. Barbs and barbed semantics for the BC setting are then introduced, and its use is shown in the encoding of mobile ambients.