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
Link To Document :
بازگشت