Development of Rabin’s Choice Coordination Algorithm in Event-B
Abstract
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.
Full Text:
PDFDOI: http://dx.doi.org/10.14279/tuj.eceasst.35.548
DOI (PDF): http://dx.doi.org/10.14279/tuj.eceasst.35.548.586
Hosted By Universitätsbibliothek TU Berlin.