This is an old revision of the document!
Title: Encoding synchronous (and asynchronous) interactions using open Petri nets
Speaker: Fabio Gadducci
Authors: Paolo Baldan, Filippo Bonchi, Fabio Gadducci, Giacoma Valentina Monreale
Abstract: The paper investigates the relationships between two well-known approaches to the modelling of concurrent and distributed systems, process calculi and Petri nets. In particular, two exemplary calculi are considered, namely asynchronous CCS and CSP, representing different interaction paradigms. A modular encoding for processes of both calculi into a reactive variant of nets is proposed and it is proved that it preserves as well
reflects the operational semantics. Since it is well behaved with respect to the standard behavioural equivalences such as trace and bisimulation ones, the encoding is then 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 net formalism and the algebraic process framework.