TY  - RPRT
CY  - Dusseldorf, Germany
ID  - deploy258
UR  - http://deploy-eprints.ecs.soton.ac.uk/258/
A1  - Yilmaz, Emre
A1  - Hoang, Thai Son
N2  - The paper reports our investigation on tool support for the integration of qualitative probabilistic reasoning into Event-B.  In the process, we formalise a non-trivial algorithm, namely Rabin's choice coordination.  Our correctness reasoning is a combination of termination proofs in terms of probabilistic convergence and standard invariant techniques.  Moreover, we describe how qualitative probabilistic reasoning can be maintained during refinement.
PB  - University of Düsseldorf
TI  - Development of Rabin's Choice Coordination Algorithm in Event-B
M1  - technical_report
AV  - public
ER  -

<script src='//archive-bar.soton.ac.uk/archive-bar.js'></script>