Of probabilistic wp and CSP - And compositionality

Abstract

We connect probabilistic Action Systems and probabilistic CSP, inducing healthiness conditions for the probabilistic traces, failures and divergences of the latter. A probabilistic sequential semantics for pGCL [31] is "inserted underneath" an existing but non-probabilistic link between action systems and CSP. Thus the link, which earlier yielded the classic CSP healthiness conditions [34], is induced to produce probabilistic versions of them "for free". Although probabilistic concurrency has enjoyed the attentions of a very large number of researchers over many years - including ourselves [37] - we nevertheless hope to gain new insights by combining the two approaches CSP and pGCL. In the meantime, however, we probably raise more questions than we answer: in particular, the issue of compositionality - for the moment - remains as delicate as ever. © Springer-Verlag Berlin Heidelberg 2005.