Carroll Morgan, Annabelle McIver, Karen Seidel, J W Sanders
October 1995, 25pp
In "Refinement oriented probability for CSP" a space PCSP of probabilistic processes is constructed uniformly from the standard CSP failures-divergences model.
Laws of CSP (whether expressing equivalence or refinement) are shown
to be valid
in PCSP also, provided they have no duplication on either
side: thus for example (writing |¯| for non-deterministic choice)
A |¯| B = B |¯| A carries over to PCSP;
but A |¯| A = A does not,
because of the duplication on its left-hand side.
Here we propose two devices for retaining more of CSP's laws within PCSP: the first introduces a limited form of state; the second allows multiple occurences of a term to be abstracted to a single syntactic location.
"Refinement oriented probability for CSP" (available as PRG Technical Report PRG-TR-12-94 or its published revision ) is prerequisite for understanding this report fully, although skimming Sec 4 and App A may give an idea of what has been achieved.