{"id":1247,"date":"2014-01-20T15:20:56","date_gmt":"2014-01-20T14:20:56","guid":{"rendered":"https:\/\/project.inria.fr\/plasma-lab\/?page_id=1247"},"modified":"2015-04-22T11:51:45","modified_gmt":"2015-04-22T09:51:45","slug":"synchronous-leader-election-protocol","status":"publish","type":"page","link":"https:\/\/project.inria.fr\/plasma-lab\/examples\/synchronous-leader-election-protocol\/","title":{"rendered":"Synchronous Leader Election protocol"},"content":{"rendered":"<p>This problem is based on the synchronous leader election protocol of Itai &amp; Rodeh [<a href=\"http:\/\/www.prismmodelchecker.org\/bibitem.php?key=IR90\">IR90<\/a>]. This protocol solves the following problem.<\/p>\n<p style=\"padding-left: 30px;\"><i>Given a synchronous ring of <b>N<\/b> processors design a protocol such that they will be able to elect a leader (a uniquely designated processor) by sending messages around the ring. <\/i><\/p>\n<p>These models were taken from the Prism case studies <a href=\"http:\/\/www.prismmodelchecker.org\/casestudies\/synchronous_leader.php\">here<\/a>. A PLASMA Lab project file containing Leader Sync models and the property used for this experiment can be downloaded <a href=\"http:\/\/plasma-lab.gforge.inria.fr\/plasma_lab_examples\/DTMC\/leader_sync.plasma\"><strong>here<\/strong><\/a>.<\/p>\n<p>We estimated the property of a leader being elected within L rounds. This property can be expressed in B-LTL as:<\/p>\n<p style=\"padding-left: 30px;\"><em>F&lt;=#(L*(N+1)) &#8220;elected&#8221;<\/em><\/p>\n<p><em>L<\/em> is the number of rounds,<em> N<\/em> is the number of processors and <em>&#8220;elected&#8221;<\/em> is a RML label expressing the fact that one leader has been elected. Here are the results of our experiments for various values of L, N and K.<\/p>\n<div id=\"attachment_1250\" style=\"width: 310px\" class=\"wp-caption aligncenter\"><a href=\"https:\/\/project.inria.fr\/plasma-lab\/files\/2014\/01\/lsync_3.png\"><img loading=\"lazy\" decoding=\"async\" aria-describedby=\"caption-attachment-1250\" class=\"size-medium wp-image-1250 \" alt=\"lsync_3\" src=\"https:\/\/project.inria.fr\/plasma-lab\/files\/2014\/01\/lsync_3-300x214.png\" width=\"300\" height=\"214\" srcset=\"https:\/\/project.inria.fr\/plasma-lab\/files\/2014\/01\/lsync_3-300x214.png 300w, https:\/\/project.inria.fr\/plasma-lab\/files\/2014\/01\/lsync_3.png 903w\" sizes=\"auto, (max-width: 300px) 100vw, 300px\" \/><\/a><p id=\"caption-attachment-1250\" class=\"wp-caption-text\">N=3<\/p><\/div>\n<div id=\"attachment_1251\" style=\"width: 310px\" class=\"wp-caption aligncenter\"><a href=\"https:\/\/project.inria.fr\/plasma-lab\/files\/2014\/01\/lsync_4.png\"><img loading=\"lazy\" decoding=\"async\" aria-describedby=\"caption-attachment-1251\" class=\"size-medium wp-image-1251 \" alt=\"lsync_4\" src=\"https:\/\/project.inria.fr\/plasma-lab\/files\/2014\/01\/lsync_4-300x210.png\" width=\"300\" height=\"210\" srcset=\"https:\/\/project.inria.fr\/plasma-lab\/files\/2014\/01\/lsync_4-300x210.png 300w, https:\/\/project.inria.fr\/plasma-lab\/files\/2014\/01\/lsync_4.png 900w\" sizes=\"auto, (max-width: 300px) 100vw, 300px\" \/><\/a><p id=\"caption-attachment-1251\" class=\"wp-caption-text\">N=4<\/p><\/div>\n<p><div id=\"attachment_1252\" style=\"width: 310px\" class=\"wp-caption aligncenter\"><a href=\"https:\/\/project.inria.fr\/plasma-lab\/files\/2014\/01\/lsync_5.png\"><img loading=\"lazy\" decoding=\"async\" aria-describedby=\"caption-attachment-1252\" class=\"size-medium wp-image-1252 \" alt=\"lsync_5\" src=\"https:\/\/project.inria.fr\/plasma-lab\/files\/2014\/01\/lsync_5-300x209.png\" width=\"300\" height=\"209\" srcset=\"https:\/\/project.inria.fr\/plasma-lab\/files\/2014\/01\/lsync_5-300x209.png 300w, https:\/\/project.inria.fr\/plasma-lab\/files\/2014\/01\/lsync_5.png 905w\" sizes=\"auto, (max-width: 300px) 100vw, 300px\" \/><\/a><p id=\"caption-attachment-1252\" class=\"wp-caption-text\">N=5<\/p><\/div><\/p>","protected":false},"excerpt":{"rendered":"<p>This problem is based on the synchronous leader election protocol of Itai &amp; Rodeh [IR90]. This protocol solves the following problem. Given a synchronous ring of N processors design a protocol such that they will be able to elect a leader (a uniquely designated processor) by sending messages around the\u2026<\/p>\n<p> <a class=\"continue-reading-link\" href=\"https:\/\/project.inria.fr\/plasma-lab\/examples\/synchronous-leader-election-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-1247","page","type-page","status-publish","hentry"],"_links":{"self":[{"href":"https:\/\/project.inria.fr\/plasma-lab\/wp-json\/wp\/v2\/pages\/1247","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=1247"}],"version-history":[{"count":7,"href":"https:\/\/project.inria.fr\/plasma-lab\/wp-json\/wp\/v2\/pages\/1247\/revisions"}],"predecessor-version":[{"id":2026,"href":"https:\/\/project.inria.fr\/plasma-lab\/wp-json\/wp\/v2\/pages\/1247\/revisions\/2026"}],"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=1247"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}