• DocumentCode
    2230092
  • Title

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

  • Author

    Degano, Pierpaolo ; De Nicola, Rocco ; Montanari, Ugo

  • Author_Institution
    Dipartimento di Inf., Pisa Univ., Italy
  • fYear
    1988
  • fDate
    0-0 1988
  • Firstpage
    133
  • Lastpage
    141
  • 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.<>
  • Keywords
    formal logic; theorem proving; calculus of communicating systems; denotational semantics; direct correspondence; event structures; occurrence nets; rewriting rules; truly concurrent operational semantics; Carbon capture and storage; Concurrent computing; Contracts; Discrete event simulation; Guidelines; History; Interleaved codes; Mathematical model; Petri nets; Testing;
  • fLanguage
    English
  • Publisher
    ieee
  • Conference_Titel
    Logic in Computer Science, 1988. LICS '88., Proceedings of the Third Annual Symposium on
  • Conference_Location
    Edinburgh, UK
  • Print_ISBN
    0-8186-0853-6
  • Type

    conf

  • DOI
    10.1109/LICS.1988.5112
  • Filename
    5112