The algebra of CSP
Bill Roscoe ( Oxford University Computing Laboratory )
- 11:30 24th February 2010 ( week 6, Hilary Term 2010 )Room 441, 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:
