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.
CITATION STYLE
Morgan, C. (2005). Of probabilistic wp and CSP - And compositionality. In Lecture Notes in Computer Science (Vol. 3525, pp. 220–241). Springer Verlag. https://doi.org/10.1007/11423348_12
Mendeley helps you to discover research relevant for your work.