Skip to main content

The algebra of CSP

Bill Roscoe ( Oxford University Computing Laboratory )

In recent years we have come to understand the hierarchy of CSP's semantic models, with options about how to treat divergence, the observation of stable behaviour, and whether the latter are made only at the ends of traces or throughout.

In this talk I will develop an algebraic semantics for the finest model (acceptance traces with non-strict divergences), which requires particular care over unstable visible actions; and show how the addition of the following laws allow one to reduce that normal form to ones for coarser models:

div = P |~| div divergence strictness
P = P |~| div finite observations only
P = P [] P from acceptance traces to refusal testing
?x:A -> (P(x) |~| Q(x)) = (?x:A -> P(x)) [> (?x:A -> Q(x)) to one-off observations of stability
P [> Q = (P |~| STOP) [] Q from revivals to failures
P|~|Q = P[]Q from failures to traces

 

This talk is based on the chapter “The algebra of CSP” from Understanding Concurrent Systems. Drafts available from the author.

Share this: