The relation between process calculi and Petri nets, two fundamental models of concurrency, has been widely investigated. Many proposals exist for encoding process calculi into Petri nets while preserving some behavioural features of interest. We recently introduced a framework where a net encoding can be defined uniformly for calculi with different communication patterns, including synchronous two-party, multiparty, and asynchronous communication. The encoding preserves and reflects several behavioural semantics, notably bisimulation equivalence. The situation is less immediate for asynchronous calculi and trace semantics: considering traces that arise when viewing asynchronous calculi as a fragment of the synchronous ones, trace equivalence is not reflected by the encoding. Focusing on CCS, we argue that this phenomenon is related to the imperfect match between trace inclusion and may testing preorder. We consider an alternative labelled transition systems where the latter issue is solved, and we show that, indeed, the corresponding trace semantics is preserved and reflected by the net encoding.

Asynchronous traces and open Petri nets

Bonchi, Filippo;GADDUCCI, FABIO;
2015-01-01

Abstract

The relation between process calculi and Petri nets, two fundamental models of concurrency, has been widely investigated. Many proposals exist for encoding process calculi into Petri nets while preserving some behavioural features of interest. We recently introduced a framework where a net encoding can be defined uniformly for calculi with different communication patterns, including synchronous two-party, multiparty, and asynchronous communication. The encoding preserves and reflects several behavioural semantics, notably bisimulation equivalence. The situation is less immediate for asynchronous calculi and trace semantics: considering traces that arise when viewing asynchronous calculi as a fragment of the synchronous ones, trace equivalence is not reflected by the encoding. Focusing on CCS, we argue that this phenomenon is related to the imperfect match between trace inclusion and may testing preorder. We consider an alternative labelled transition systems where the latter issue is solved, and we show that, indeed, the corresponding trace semantics is preserved and reflected by the net encoding.
Baldan, Paolo; Bonchi, Filippo; Gadducci, Fabio; Monreale, Giacoma Valentina
File in questo prodotto:
File Dimensione Formato  
degano.pdf

solo utenti autorizzati

Descrizione: Articolo principale
Tipologia: Versione finale editoriale
Licenza: NON PUBBLICO - Accesso privato/ristretto
Dimensione 501.89 kB
Formato Adobe PDF
501.89 kB Adobe PDF   Visualizza/Apri   Richiedi una copia

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11568/792986
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 3
  • ???jsp.display-item.citation.isi??? 2
social impact