--- 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." accompaniment: [] book_title: ~ commentary: ~ completion_time: ~ composition_type: ~ conductors_id: [] conductors_name: [] contact_email: ~ copyright_holders: [] corp_creators: [] creators_id: - ~ - htson@inf.ethz.ch creators_name: - family: Yilmaz given: Emre honourific: '' lineage: '' - family: Hoang given: Thai Son honourific: '' lineage: '' data_type: ~ date: ~ date_type: ~ datestamp: 2010-12-01 11:08:34 department: ~ dir: disk0/00/00/02/58 divisions: [] edit_lock_since: ~ edit_lock_until: 0 edit_lock_user: ~ editors_id: [] editors_name: [] eprint_status: archive eprintid: 258 event_dates: ~ event_location: ~ event_title: ~ event_type: ~ exhibitors_id: [] exhibitors_name: [] fileinfo: /style/images/fileicons/application_pdf.png;/258/1/rabin%2Dllncs.pdf full_text_status: public funders: [] id_number: ~ importid: ~ institution: University of Düsseldorf isbn: ~ ispublished: pub issn: ~ item_issues_comment: [] item_issues_count: 0 item_issues_description: [] item_issues_id: [] item_issues_reported_by: [] item_issues_resolved_by: [] item_issues_status: [] item_issues_timestamp: [] item_issues_type: [] keywords: ~ lastmod: 2010-12-09 15:37:25 latitude: ~ learning_level: ~ longitude: ~ lyricists_id: [] lyricists_name: [] metadata_visibility: show monograph_type: technical_report note: ~ num_pieces: ~ number: ~ official_url: ~ output_media: ~ pagerange: ~ pages: ~ patent_applicant: ~ pedagogic_type: ~ place_of_pub: 'Dusseldorf, Germany' pres_type: ~ producers_id: [] producers_name: [] projects: [] publication: ~ publisher: University of Düsseldorf refereed: ~ referencetext: ~ related_url_type: [] related_url_url: [] relation_type: [] relation_uri: [] rev_number: 17 series: ~ skill_areas: [] source: ~ status_changed: 2010-12-01 11:08:34 subjects: - deploy_tooldev_rodinplugins - examples succeeds: ~ suggestions: ~ sword_depositor: ~ sword_slug: ~ task_purpose: ~ thesis_type: ~ title: Development of Rabin's Choice Coordination Algorithm in Event-B type: monograph userid: 16 volume: ~