REVIEW 1 cited by
Structure Preserving Bisimilarity, Supporting an Operational Petri Net Semantics of CCSP
Not yet reviewed by Pith; the record is open.
This paper has not been read by Pith yet. Machine review is queued; the pith claim, tier, and objections will appear here once it completes.
SPECIMEN: schema-true, not a live event
T0 review · schema-true
One-sentence machine reading of the paper's core claim.
pith:XXXXXXXX · record.json · timestamp
Signed reviews
read the original abstract
In 1987 Ernst-R\"udiger 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.
Forward citations
Cited by 1 Pith paper
-
Justness: A Completeness Criterion for Capturing Liveness Properties
This paper defines a synchron-based concurrency relation for CCS, ABC, and CCSS, making the justness criterion formally available and proving it agrees with previous coinductive definitions.
Discussion (0). Continue with ORCID to comment.