The talk presents a personal recollection of recent results on the synthesis of labelled transition systems (\textsc{lts}s) for process calculi.

The starting point are the graphical techniques introduced by the speaker and Ugo Montanari for modelling the reduction semantics of nominal calculi: processes are mapped into graphs equipped with suitable \emph{interfaces}, such that the denotation is fully abstract with respect to the usual structural congruence. Moreover, the use of non hierarchical graphs allows for the reuse of standard graph rewriting theory and tools for simulating the reduction semantics of the calculus, such as the \emph{double pushout} (\textsc{dpo}) approach and the associated concurrent semantics (which allows for the simultaneous execution of independent reductions, thus implicitly defining a non-deterministic concurrent semantics).

Another relevant fact is the use of  \emph{cospan categories} for simulating \textsc{dpo} rewriting, proposed by the speaker with Reiko Heckel and Merce Llabres Segura. A cospan over the category of graphs is just a pair of arrows with the same target. To each production in the \textsc{dpo} style a pair of cospans is associated;  then, \textsc{dpo} rewrites are captured by an inductive closure of the set of pairs of cospans, mirroring the dichotomy between the operational and the algebraic description of term rewriting.

A third component is the fact that graph with interfaces are just an instance of a cospan category (over the category of graphs). Hence, graphs with interfaces are amenable to the synthesis mechanism based on \emph{borrowed contexts} (\textsc{bc}s), proposed by Ehrig and Koenig (which are in turn an instance of \emph{relative pushouts}, originally introduced by Milner and Leifer). The \textsc{bc} mechanism allows the effective construction of an \textsc{lts} that has graphs with interfaces as both states and labels, and such that the associated bisimilarity is automatically a congruence. 

So; since the category of cospans over graphs admits \textsc{rpo}s (as proved by Sassone and Sobocinski), its choice as the domain of the encoding for nominal calculi ensures that the synthesis of an \textsc{lts} can be performed, and that a \emph{compositional} observational equivalence is obtained. The talk discusses the analysis of the \textsc{lts} distilled by exploiting the encoding of \textsc{ccs} processes: besides offering some technical contributions towards the simplification of the \textsc{bc} mechanism, the key result of this joint work with Bonchi and Koenig is the proof that the bisimilarity on (encondings of) processes obtained via \textsc{bc}s coincides with the standard strong bisimilarity for \textsc{ccs}.