Among the many opportunities offered by computational semantics for probability, the challenge of probabilistic Event B (pEB) is one of the most attractive.
The B method itself is now almost 20 years old, and has been much improved and adapted over that time by the many projects to which it has been applied, and by its philosophy —right from the start— that it must be practical, effective and amenable to tool support.; more recently, Event B has extended it and altered its style of use. The probabilistic-program semantics we appeal to is even older (in Kozens original form), but has only recently been revived in the context of B-style abstraction and refinement. The especial attraction of putting the two together is the likely interplay between the probabilistic theory, on the one hand, and the decades of practical experience that have by now been built-in to the B approach, on the other.
In particular, there are areas where a full theoretical treatment of probability, concurrency, abstraction and refinement —all at once— seems prohibitively complex; and yet in practice either the complexities seldom occur, or the exigencies of Bs having been so-often applied to real, non-toy problems has forced it to evolve styles for avoiding such complexities. In short, we want to use (event) B to guide us towards the issues that truly are important.
Rabins randomized mutual-exclusion algorithm is used as a motivating case study.