Modular encoding of synchronous and asynchronous interactions using open Petri nets

•A Petri net encoding for process calculi and their operational/behavioural semantics•A formal assessment and comparison of synchronous and asynchronous interaction paradigms•A methodology for the sound transfer of tools and techniques between Petri nets and process calculi

The paper investigates the relationships between two well-known approaches to the modelling of concurrent and distributed systems, process calculi and Petri nets. A framework for the modular encoding of process calculi into Petri nets is proposed, which is based on a reactive variant of Petri nets. In particular, two exemplary calculi are considered: (asynchronous) CCS and CSP, representing alternative interaction paradigms, namely asynchronous and (broadcast) synchronous communication. The encoding is proved to preserve as well as to reflect the operational semantics. As a consequence, it is well-behaved with respect to the standard behavioural equivalences, a fact that is exploited to perform a “technology transfer” between the two formalisms, in terms of un/decidability results for classical properties such as reachability and deadlock-freedom.The encoding highlights the expressiveness of the proposed reactive variant of nets, as well as paving the way for a fruitful integration of tools and techniques between the visual formalism of nets and the algebraic framework of processes.