User Tools

Site Tools


talkgadducci

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

Both sides previous revision Previous revision
Next revision
Previous revision
talkgadducci [2014/07/22 10:30]
unige
talkgadducci [2014/07/22 10:48]
unige
Line 1: Line 1:
-**Title:** Encoding synchronous ​(and asynchronousinteractions using open Petri nets+**Title:** Encoding synchronous and asynchronous interactions using open Petri nets
  
 **Speaker:​** Fabio Gadducci **Speaker:​** Fabio Gadducci
Line 5: Line 5:
 **Authors:​** Paolo Baldan, Filippo Bonchi, Fabio Gadducci, Giacoma Valentina Monreale **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 ​(asynchronousCCS 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 +**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. \\ 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. 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.
  
talkgadducci.txt ยท Last modified: 2014/07/22 10:48 by unige