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

Select |




Print


van Glabbeek, Robert

van Glabbeek, Robert


2015-09-08


Conference Material


Correct System Design - Symposium in Honor of Ernst-Rüdiger Olderog on the Occasion of His 60th Birthday


Oldenburg, Germany


99-130


In 1987 Ernst-Rdiger 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. This paper strengthens (2), employing a novel branching-time version of this semantics ---structure preserving bisimilarity---that moreover preserves inevitability. I establish that it is a congruence for the operators of CCSP.


Springer


Petri nets, concurrency, process algebra, operational semantics, semantic equivalences, inevitability


https://doi.org/10.1007/978-3-319-23506-6_9


https://www.uni-oldenburg.de/informatik/csd/festschrift/


© 2015


LNCS


English


nicta:8776


van Glabbeek, Robert. Structure Preserving Bisimilarity, Supporting an Operational Petri Net Semantics of CCSP. In: R. Meyer, A. Platzer & H. Wehrheim Editor, editor/s. Correct System Design - Symposium in Honor of Ernst-Rüdiger Olderog on the Occasion of His 60th Birthday; Oldenburg, Germany. Springer; 2015-09-08. 99-130. https://doi.org/10.1007/978-3-319-23506-6_9



Loading citation data...

Citation counts
(Requires subscription to view)