Structure Preserving Bisimilarity, Supporting an Operational Petri Net Semantics of CCSP

Research output: Chapter in Book/Report/Conference proceedingChapter (peer-reviewed)peer-review

Abstract / Description of output

In 1987 Ernst-Rüdiger Olderog provided an operational Petri net semantics for a subset of CCSP, the union of Milner's CCS and Hoare's CSP. It assigns to each process term in the subset a labelled, safe place/transition net. To demonstrate the correctness of the approach, Olderog established agreement (1) with the standard interleaving semantics of CCSP up to strong bisimulation equivalence, and (2) with standard denotational interpretations of CCSP operators in terms of Petri nets up to a suitable semantic equivalence that fully respects the causal structure of nets. For the latter he employed a linear-time semantic equivalence, namely having the same causal nets.
Original languageEnglish
Title of host publicationCorrect System Design: Symposium in Honor of Ernst-Rüdiger Olderog on the Occasion of His 60th Birthday, Oldenburg, Germany, September 8-9, 2015, Proceedings
EditorsRoland Meyer, André Platzer, Heike Wehrheim
Place of PublicationCham
PublisherSpringer International Publishing
Pages99-130
Number of pages32
ISBN (Electronic)978-3-319-23506-6
ISBN (Print)978-3-319-23505-9
DOIs
Publication statusPublished - 10 Nov 2015
EventSymposium in Honor of Ernst-Rüdiger Olderog on the Occasion of His 60th Birthday, 2015 - Oldenburg, Germany
Duration: 8 Sept 20159 Sept 2015

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Cham
Volume9360
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Symposium

SymposiumSymposium in Honor of Ernst-Rüdiger Olderog on the Occasion of His 60th Birthday, 2015
Country/TerritoryGermany
CityOldenburg
Period8/09/159/09/15

Fingerprint

Dive into the research topics of 'Structure Preserving Bisimilarity, Supporting an Operational Petri Net Semantics of CCSP'. Together they form a unique fingerprint.

Cite this