Programming Research Group Technical Report TR-12-94

Carroll Morgan, Annabelle McIver, Karen Seidel, and J W Sanders

August 1994, 47pp.

Probability is introduced into CSP by generalising the notion of refinement, from the discrete "either implements, or does not" to the continuous "implements with some probability". That contrasts with the operational approach, where instead it is the execution of processes that is made probabilistic.

Our refinement-oriented approach allows a uniform embedding of all standard CSP operators, including demonic nondeterminism, into a probabilistic space. A large number of the algebraic laws of CSP embed similarly, and simple syntactic criteria can be given for identifying those that do.

The basis of explicit probability is an extra operator, probabilistic choice p(+), that selects its left operand with probability p. Probabilistic choice is shown to distribute through all standard operators, including nondeterminism.

A simple communications protocol is used to illustrate the resulting algebra.