Modular encoding of synchronous and asynchronous interactions using open Petri nets

摘要

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.