The Challenge of Probabilistic Event B—Extended Abstract—
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, EventB has extended it and altered its style of use. The probabilistic-program semantics we appeal to is even older (in Kozen’s 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 B’s 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.
Rabin’s randomized mutual-exclusion algorithm is used as a motivating case study.
KeywordsProbabilistic Event Critical Section Mutual Exclusion Probabilistic Choice Predicate Transformer
Unable to display preview. Download preview PDF.
- 3.Butler, M.J.: A CSP approach to action systems. DPhil thesis, Computing Lab., Oxford University (1992)Google Scholar
- 5.Chen, W., Udding, J.T.: Towards a calculus of data refinement. In: van de Snepscheut, J.L.A. (ed.) MPC 1989. LNCS, vol. 375. Springer, Heidelberg (1989)Google Scholar
- 7.Gries, D., Prins, J.: A new notion of encapsulation. In: Symposium on Language Issues in Programming Environments, SIGPLAN (June 1985)Google Scholar
- 8.He, J., Hoare, C.A.R., Sanders, J.W.: Data refinement refined. In: Robinet, B., Wilhelm, R. (eds.) ESOP 1986. LNCS, vol. 213, pp. 187–196. Springer, Heidelberg (1986)Google Scholar
- 10.Hoang, T.S., Jin, Z., Robinson, K., McIver, A., Morgan, C., Hoang, T.S.: Development via refinement in probabilistic B — foundation and case study. LNCS. Springer, HiedelbergGoogle Scholar
- 11.Hoang, T.S., Jin, Z., Robinson, K., McIver, A., Morgan, C., Hoang, T.S.: Probabilistic invariants for probabilistic machines. In: Bert et al.Google Scholar
- 14.Kushilevitz, E., Rabin, M.O.: Randomized mutual exclusion algorithms revisited. In: Proc. 11th Annual ACM Symp. on Principles of Distributed Computing (1992)Google Scholar
- 15.McIver, A.K., Morgan, C.C., Sanders, J.W., Seidel, K.: Probabilistic Systems Group: Collected reports, web.comlab.ox.ac.uk/oucl/research/areas/probs
- 16.McIver, A., Morgan, C.: Abstraction, Refinement and Proof for Probabilistic Systems. In: Technical Monographs in Computer Science. Springer, New York (2004)Google Scholar
- 17.McIver, A., Morgan, C., Hoang, T.S.: Probabilistic termination in B. In: Bert et al. Google Scholar
- 20.Morgan, C.C.: Of wp and CSP. In: Feijen, W.H.J., et al. (eds.) Beauty is Our Business. Springer, Heidelberg (1990)Google Scholar
- 22.Morgan, C.C., Vickers, T.N. (eds.): On the Refinement Calculus. FACIT Series in Computer Science. Springer, London (1994)Google Scholar
- 26.Saias, I.: Proving probabilistic correctness statements: the case of Rabin’s algorithm for mutual exclusion. In: Proc. 11th Annual ACM Symp. on Principles of Distributed Computing (1992)Google Scholar