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

Abstract

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. 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.

References in corpus (3)

• A Process Algebra for Wireless Mesh Networks used for Modelling, Verifying and Analysing AODV
• CCS: It's not Fair! Fair Schedulers cannot be implemented in CCS-like languages even under progress and certain fairness assumptions
• Progress, Fairness and Justness in Process Algebra

Cited by in corpus (6)

• Ensuring Liveness Properties of Distributed Systems: Open Problems
• Ensuring Liveness Properties of Distributed Systems (A Research Agenda)
• Justness: A Completeness Criterion for Capturing Liveness Properties
• Place Bisimilarity is Decidable, Indeed!
• Decidability of Two Truly Concurrent Equivalences for Finite Bounded Petri Nets
• A Decidable Equivalence for a Turing-complete, Distributed Model of Computation