{"id":1095,"date":"2013-10-10T11:23:09","date_gmt":"2013-10-10T09:23:09","guid":{"rendered":"https:\/\/project.inria.fr\/plasma-lab\/?page_id=1095"},"modified":"2016-07-01T16:13:29","modified_gmt":"2016-07-01T14:13:29","slug":"consensus-protocol","status":"publish","type":"page","link":"https:\/\/project.inria.fr\/plasma-lab\/examples\/consensus-protocol\/","title":{"rendered":"Randomised Consensus Shared Coin Protocol"},"content":{"rendered":"<p>This case study concerns modeling and verifying the shared coin protocol of the randomised consensus algorithm of Aspnes and Herlihy [<a href=\"http:\/\/www.prismmodelchecker.org\/bibitem.php?key=AH90\">AH90<\/a>] using the RML language.<\/p>\n<p>This case study was taken from the Prism case studies <a href=\"http:\/\/www.prismmodelchecker.org\/casestudies\/consensus_prism.php\">here<\/a>.<\/p>\n","protected":false},"excerpt":{"rendered":"<p>This case study concerns modeling and verifying the shared coin protocol of the randomised consensus algorithm of Aspnes and Herlihy [AH90] using the RML language. This case study was taken from the Prism case studies here.<\/p>\n<p> <a class=\"continue-reading-link\" href=\"https:\/\/project.inria.fr\/plasma-lab\/examples\/consensus-protocol\/\"><span>Continue reading<\/span><i class=\"crycon-right-dir\"><\/i><\/a> <\/p>\n","protected":false},"author":234,"featured_media":0,"parent":236,"menu_order":0,"comment_status":"closed","ping_status":"open","template":"","meta":{"footnotes":""},"class_list":["post-1095","page","type-page","status-publish","hentry"],"_links":{"self":[{"href":"https:\/\/project.inria.fr\/plasma-lab\/wp-json\/wp\/v2\/pages\/1095","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/project.inria.fr\/plasma-lab\/wp-json\/wp\/v2\/pages"}],"about":[{"href":"https:\/\/project.inria.fr\/plasma-lab\/wp-json\/wp\/v2\/types\/page"}],"author":[{"embeddable":true,"href":"https:\/\/project.inria.fr\/plasma-lab\/wp-json\/wp\/v2\/users\/234"}],"replies":[{"embeddable":true,"href":"https:\/\/project.inria.fr\/plasma-lab\/wp-json\/wp\/v2\/comments?post=1095"}],"version-history":[{"count":15,"href":"https:\/\/project.inria.fr\/plasma-lab\/wp-json\/wp\/v2\/pages\/1095\/revisions"}],"predecessor-version":[{"id":2176,"href":"https:\/\/project.inria.fr\/plasma-lab\/wp-json\/wp\/v2\/pages\/1095\/revisions\/2176"}],"up":[{"embeddable":true,"href":"https:\/\/project.inria.fr\/plasma-lab\/wp-json\/wp\/v2\/pages\/236"}],"wp:attachment":[{"href":"https:\/\/project.inria.fr\/plasma-lab\/wp-json\/wp\/v2\/media?parent=1095"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}