The problem of the relationships between "truly concurrent" operational and denotational semantics is tackled by mapping syntactic terms on similar semantic domains in both approaches. Occurrence Nets are associated to terms through a structured operational semantics based on a set of rewriting rules; Event Structures are defined as denotations for terms, without resorting to categorical constructions. The proof of the equivalence of the two semantics relies on the direct correspondence between Occurrence Nets and Event Structures. As a test case we use Milner's CCS: "truly concurrent's denotational and operational semantics are given for it and proved consistent. This equivalence is established here for the first time in the the concurrency approach. We prove also thal Winskel's categorical denotational semantics is equivalent to ours.

On the consistency of 'truly concurrent' operational and denotational semantics

De Nicola R;
1988

Abstract

The problem of the relationships between "truly concurrent" operational and denotational semantics is tackled by mapping syntactic terms on similar semantic domains in both approaches. Occurrence Nets are associated to terms through a structured operational semantics based on a set of rewriting rules; Event Structures are defined as denotations for terms, without resorting to categorical constructions. The proof of the equivalence of the two semantics relies on the direct correspondence between Occurrence Nets and Event Structures. As a test case we use Milner's CCS: "truly concurrent's denotational and operational semantics are given for it and proved consistent. This equivalence is established here for the first time in the the concurrency approach. We prove also thal Winskel's categorical denotational semantics is equivalent to ours.
1988
Istituto di Scienza e Tecnologie dell'Informazione "Alessandro Faedo" - ISTI
0818608536
Truly concurrent
Operational and denotational semantics
File in questo prodotto:
File Dimensione Formato  
prod_419405-doc_148206.pdf

solo utenti autorizzati

Descrizione: On the consistency of 'truly concurrent' operational and denotational semantics
Tipologia: Versione Editoriale (PDF)
Dimensione 1.83 MB
Formato Adobe PDF
1.83 MB 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/20.500.14243/363823
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 33
  • ???jsp.display-item.citation.isi??? ND
social impact