Modular encoding of synchronous and asynchronous interactions using open Petri nets

作者：Baldan Paolo; Bonchi Filippo; Gadducci Fabio^*; Monreale Giacoma Valentina

来源：Science of Computer Programming, 2015, 109: 96-124.

DOI：10.1016/j.scico.2014.11.019

• Open Petri nets
• Asynchronous CCS
• CSP
• Net encoding of processes
• Synchronous and asynchronous interaction

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.

• 出版日期2015-10-1
• 单位INRIA