Logic in Computer Science (LICS 1988)

Paper: On the consistency of `truly concurrent' operational and denotational semantics (at LICS 1988)

Authors: Pierpaolo Degano Rocco De Nicola Ugo Montanari

Abstract

The problem of the relationship 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 structural 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. R. Milner's (1980) calculus of communicating systems is used as a test case; truly concurrent denotional and operational semantics are given for it and proved consistent. This equivalence is established for the first time in true concurrency approach. It is proved that G. Winskel's (1982) categorical denotational semantics is equivalent to that given here

BibTeX

  @InProceedings{DeganoDeNicolaMonta-Ontheconsistencyoft,
    author = 	 {Pierpaolo Degano and Rocco De Nicola and Ugo Montanari},
    title = 	 {On the consistency of `truly concurrent' operational and denotational semantics },
    booktitle =  {Proceedings of the Third Annual IEEE Symp. on Logic in Computer Science, {LICS} 1988},
    year =	 1988,
    editor =	 {Yuri Gurevich},
    month =	 {July}, 
    pages =      {133--141},
    location =   {Edinburgh, Scotland, UK}, 
    publisher =	 {IEEE Computer Society Press}
  }