{"id":1096,"date":"2013-10-10T11:23:46","date_gmt":"2013-10-10T09:23:46","guid":{"rendered":"https:\/\/project.inria.fr\/plasma-lab\/?page_id=1096"},"modified":"2015-03-17T17:51:23","modified_gmt":"2015-03-17T16:51:23","slug":"probabilistic-broadcast-protocols","status":"publish","type":"page","link":"https:\/\/project.inria.fr\/plasma-lab\/examples\/probabilistic-broadcast-protocols\/","title":{"rendered":"Probabilistic Broadcast protocols"},"content":{"rendered":"<p>This is a simple protocol that uses probabilistic broadcast to send information in a network. This model defines nodes that will forward a received message to their neighbour with probability <em>psend<\/em> and ignore the message with probability <em>1-psend<\/em>. The model is initialized with the node 0 receiving the message.<\/p>\n<p>These models were taken from the Prism case studies <a href=\"http:\/\/www.prismmodelchecker.org\/casestudies\/prob_broadcast.php\">here<\/a>.<\/p>\n<div id=\"attachment_1117\" style=\"width: 310px\" class=\"wp-caption aligncenter\"><a href=\"https:\/\/project.inria.fr\/plasma-lab\/files\/2013\/10\/broadcast.png\"><img loading=\"lazy\" decoding=\"async\" aria-describedby=\"caption-attachment-1117\" class=\"size-medium wp-image-1117 \" alt=\"broadcast\" src=\"https:\/\/project.inria.fr\/plasma-lab\/files\/2013\/10\/broadcast-300x295.png\" width=\"300\" height=\"295\" srcset=\"https:\/\/project.inria.fr\/plasma-lab\/files\/2013\/10\/broadcast-300x295.png 300w, https:\/\/project.inria.fr\/plasma-lab\/files\/2013\/10\/broadcast.png 988w\" sizes=\"auto, (max-width: 300px) 100vw, 300px\" \/><\/a><p id=\"caption-attachment-1117\" class=\"wp-caption-text\">Network configuration with 9 nodes<\/p><\/div>\n<p style=\"text-align: center;\">Download<a href=\"http:\/\/plasma-lab.gforge.inria.fr\/plasma_lab_examples\/DTMC\/Broadcast_Protocol.plasma\"> <strong>Probabilistic_Broadcast.plasma<\/strong><\/a><\/p>\n<p style=\"text-align: justify;\">The properties we checked was with what propability does a node receive a message. The variable active_i_ eventually becomes equal to 0 when the node_i_ receives the message.<\/p>\n<p style=\"text-align: left;\"><div class=\"alert alert-success\" role=\"alert\"><p class=\"printonly\"><strong>Important!<\/strong><\/p><\/p>\n<p style=\"text-align: left;\" class=\"first-p\">F&lt;=#1000 active0=0<\/p>\n<p>F&lt;=#1000 active1=0<\/p>\n<p>F&lt;=#1000 active2=0<\/p>\n<p>F&lt;=#1000 active3=0<\/p>\n<p>F&lt;=#1000 active4=0<\/p>\n<p>F&lt;=#1000 active5=0<\/p>\n<p>F&lt;=#1000 active6=0<\/p>\n<p>F&lt;=#1000 active7=0<\/p>\n<p>F&lt;=#1000 active8=0<\/p>\n<p style=\"text-align: justify;\"><\/div><\/p>\n<p style=\"text-align: justify;\">Each one of the properties describe the event that a node will receive a message before 1000 simulations steps.<\/p>\n<p style=\"text-align: justify;\">We added an optimization directive to one of the properties:<\/p>\n<p style=\"text-align: justify;\"><div class=\"alert alert-success\" role=\"alert\"><p class=\"printonly\"><strong>Important!<\/strong><\/p>Optimize(psend = [0;1;0.2])<\/div><\/p>\n<p style=\"text-align: justify;\">This allowed us to check each of these properties for different values of psend, the probability of transmitting a message. We used the montecarlo algorithm with a parameter of 1000 simulations.<\/p>\n<p style=\"text-align: left;\"><a href=\"https:\/\/project.inria.fr\/plasma-lab\/files\/2013\/10\/pbp.png\"><img loading=\"lazy\" decoding=\"async\" class=\"size-medium wp-image-1114 aligncenter\" alt=\"pbp\" src=\"https:\/\/project.inria.fr\/plasma-lab\/files\/2013\/10\/pbp-300x285.png\" width=\"300\" height=\"285\" srcset=\"https:\/\/project.inria.fr\/plasma-lab\/files\/2013\/10\/pbp-300x285.png 300w, https:\/\/project.inria.fr\/plasma-lab\/files\/2013\/10\/pbp.png 597w\" sizes=\"auto, (max-width: 300px) 100vw, 300px\" \/><\/a><\/p>\n<p><\/p>","protected":false},"excerpt":{"rendered":"<p>This is a simple protocol that uses probabilistic broadcast to send information in a network. This model defines nodes that will forward a received message to their neighbour with probability psend and ignore the message with probability 1-psend. The model is initialized with the node 0 receiving the message. These\u2026<\/p>\n<p> <a class=\"continue-reading-link\" href=\"https:\/\/project.inria.fr\/plasma-lab\/examples\/probabilistic-broadcast-protocols\/\"><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-1096","page","type-page","status-publish","hentry"],"_links":{"self":[{"href":"https:\/\/project.inria.fr\/plasma-lab\/wp-json\/wp\/v2\/pages\/1096","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=1096"}],"version-history":[{"count":10,"href":"https:\/\/project.inria.fr\/plasma-lab\/wp-json\/wp\/v2\/pages\/1096\/revisions"}],"predecessor-version":[{"id":1948,"href":"https:\/\/project.inria.fr\/plasma-lab\/wp-json\/wp\/v2\/pages\/1096\/revisions\/1948"}],"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=1096"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}