{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,8]],"date-time":"2024-09-08T05:27:28Z","timestamp":1725773248766},"reference-count":19,"publisher":"Association for Computing Machinery (ACM)","issue":"3","content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["SIGMETRICS Perform. Eval. Rev."],"published-print":{"date-parts":[[2008,11,30]]},"abstract":"Gossip protocols have been proposed as a robust and efficient method for disseminating information throughout dynamically changing networks. We present an analysis of a gossip protocol using probabilistic model checking and the tool PRISM. Since the behaviour of these protocols is both probabilistic and nondeterministic in nature, this provides a good example of the exhaustive, quantitative analysis that probabilistic model checking techniques can provide. In particular, we compute minimum and maximum values, representing the best- and worst-case performance of the protocol under any scheduling, and investigate both their relationship with the average values that would be obtained through simulation and the precise scheduling which achieve these values.<\/jats:p>","DOI":"10.1145\/1481506.1481511","type":"journal-article","created":{"date-parts":[[2008,12,30]],"date-time":"2008-12-30T17:45:31Z","timestamp":1230659131000},"page":"17-22","update-policy":"http:\/\/dx.doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":40,"title":["Analysis of a gossip protocol in PRISM"],"prefix":"10.1145","volume":"36","author":[{"given":"Marta","family":"Kwiatkowska","sequence":"first","affiliation":[{"name":"Oxford University Computing Laboratory, Wolfson Building, Oxford"}]},{"given":"Gethin","family":"Norman","sequence":"additional","affiliation":[{"name":"Oxford University Computing Laboratory, Wolfson Building, Oxford"}]},{"given":"David","family":"Parker","sequence":"additional","affiliation":[{"name":"Oxford University Computing Laboratory, Wolfson Building, Oxford"}]}],"member":"320","published-online":{"date-parts":[[2008,11,30]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2003.1205180"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/s004460050046"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/1317379.1317385"},{"key":"e_1_2_1_4_1","series-title":"LNCS","first-page":"499","volume-title":"Proc. FST&TCS'95","author":"Bianco A.","year":"1995","unstructured":"A. Bianco and L. de Alfaro . Model checking of probabilistic and nondeterministic systems . In Proc. FST&TCS'95 , volume 1026 of LNCS , pages 499 -- 513 . Springer , 1995 . A. Bianco and L. de Alfaro. Model checking of probabilistic and nondeterministic systems. In Proc. FST&TCS'95, volume 1026 of LNCS, pages 499--513. Springer, 1995."},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-006-0014-x"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.5555\/2090188.2090204"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01211866"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/11691372_29"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/1275517.1275520"},{"key":"e_1_2_1_10_1","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4684-9455-6","volume-title":"Denumerable Markov Chains","author":"Kemeny J.","year":"1976","unstructured":"J. Kemeny , J. Snell , and A. Knapp . Denumerable Markov Chains . Springer-Verlag , 2 nd edition, 1976 . J. Kemeny, J. Snell, and A. Knapp. Denumerable Markov Chains. Springer-Verlag, 2nd edition, 1976.","edition":"2"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1109\/QEST.2006.19"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/11817963_23"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-006-0005-2"},{"key":"e_1_2_1_14_1","series-title":"LNCS","first-page":"169","volume-title":"Proc. PAPM\/PROBMIV'02","author":"Kwiatkowska M.","year":"2002","unstructured":"M. Kwiatkowska , G. Norman , and J. Sproston . Probabilistic model checking of the IEEE 802.11 wireless local area net work protocol . In Proc. PAPM\/PROBMIV'02 , volume 2399 of LNCS , pages 169 -- 187 . Springer , 2002 . M. Kwiatkowska, G. Norman, and J. Sproston. Probabilistic model checking of the IEEE 802.11 wireless local area net work protocol. In Proc. PAPM\/PROBMIV'02, volume 2399 of LNCS, pages 169--187. Springer, 2002."},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2007.01.004"},{"key":"e_1_2_1_16_1","unstructured":"PRISM web site. www.prismmodelchecker.org. PRISM web site. www.prismmodelchecker.org."},{"key":"e_1_2_1_17_1","series-title":"CRM Monograph Series","doi-asserted-by":"crossref","DOI":"10.1090\/crmm\/023","volume-title":"Mathematical Techniques for Analyzing Concurrent and Probabilistic Systems","author":"Rutten J.","year":"2004","unstructured":"J. Rutten , M. Kwiatkowska , G. Norman , and D. Parker . Mathematical Techniques for Analyzing Concurrent and Probabilistic Systems , P. Panangaden and F. van Breugel (eds.), volume 23 of CRM Monograph Series . AMS , 2004 . J. Rutten, M. Kwiatkowska, G. Norman, and D. Parker. Mathematical Techniques for Analyzing Concurrent and Probabilistic Systems, P. Panangaden and F. van Breugel (eds.), volume 23 of CRM Monograph Series. AMS, 2004."},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1109\/QEST.2007.33"},{"key":"e_1_2_1_19_1","first-page":"101","volume-title":"Proc. WONS'08","author":"Werner F.","year":"2008","unstructured":"F. Werner and P. Schmitt . Analysis of the authenticated query ooding protocol by probabilistic means . In Proc. WONS'08 , pages 101 -- 104 , 2008 . F. Werner and P. Schmitt. Analysis of the authenticated query ooding protocol by probabilistic means. In Proc. WONS'08, pages 101--104, 2008."}],"container-title":["ACM SIGMETRICS Performance Evaluation Review"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1481506.1481511","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,12,29]],"date-time":"2022-12-29T09:41:39Z","timestamp":1672306899000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1481506.1481511"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008,11,30]]},"references-count":19,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2008,11,30]]}},"alternative-id":["10.1145\/1481506.1481511"],"URL":"https:\/\/doi.org\/10.1145\/1481506.1481511","relation":{},"ISSN":["0163-5999"],"issn-type":[{"value":"0163-5999","type":"print"}],"subject":[],"published":{"date-parts":[[2008,11,30]]},"assertion":[{"value":"2008-11-30","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}