Trustworthy Systems

A branching time model of CSP

Authors

Rob van Glabbeek

DATA61

UNSW Sydney

Abstract

I present a branching time model of CSP that is finer than all other models of CSP proposed thus far. It is obtained by taking a semantic equivalence from the linear time -- branching time spectrum, namely divergence-preserving coupled similarity, and showing that it is a congruence for the operators of CSP. This equivalence belongs to the bisimulation family of semantic equivalences, in the sense that on transition systems without internal actions it coincides with strong bisimilarity. Nevertheless, enough of the equational laws of CSP remain to obtain a complete axiomatisation for closed, recursion-free terms.

BibTeX Entry

  @inbook{vanGlabbeek_17,
    address          = {Uppsala, Sweden},
    author           = {van Glabbeek, Robert},
    booktitle        = {Concurrency, Security, and Puzzles - Essays Dedicated to Andrew William Roscoe on the Occasion of
                        His 60th Birthday},
    date             = {2017-1-9},
    doi              = {https://doi.org/10.1007/978-3-319-51046-0\_14},
    isbn             = {9783319510453},
    keywords         = {Process algebra; Communicating Sequential Processes ({CSP}); Structural Operational Semantics;
                        Branching time semantics; Coupled simulation; Complete axiomatisations},
    month            = jan,
    pages            = {272-293},
    paperurl         = {https://trustworthy.systems/publications/full_text/vanGlabbeek_17.pdf},
    publisher        = {Springer},
    series           = {Lecture Notes in Computer Science},
    title            = {{A} Branching Time Model of {CSP}},
    volume           = {10160},
    year             = {2017}
  }

Download