{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,11]],"date-time":"2025-10-11T17:10:50Z","timestamp":1760202650905},"reference-count":21,"publisher":"Association for Computing Machinery (ACM)","issue":"4-6","license":[{"start":{"date-parts":[[2012,7,1]],"date-time":"2012-07-01T00:00:00Z","timestamp":1341100800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2012,7]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>\n            Herman\u2019s self-stabilisation algorithm provides a simple randomised solution to the problem of recovering from faults in an\n            <jats:italic>N<\/jats:italic>\n            -process token ring. However, a precise analysis of the algorithm\u2019s maximum execution time proves to be surprisingly difficult. McIver and Morgan have conjectured that the worst-case behaviour results from a ring configuration of three evenly spaced tokens, giving an expected time of approximately 0.15\n            <jats:italic>N<\/jats:italic>\n            <jats:sup>2<\/jats:sup>\n            . However, the tightest upper bound proved to date is 0.64\n            <jats:italic>N<\/jats:italic>\n            <jats:sup>2<\/jats:sup>\n            . We apply probabilistic verification techniques, using the probabilistic model checker PRISM, to analyse the conjecture, showing it to be correct for all sizes of the ring that can be exhaustively analysed. We furthermore demonstrate that the worst-case execution time of the algorithm can be reduced by using a biased coin.\n          <\/jats:p>","DOI":"10.1007\/s00165-012-0227-6","type":"journal-article","created":{"date-parts":[[2012,6,28]],"date-time":"2012-06-28T08:35:50Z","timestamp":1340872550000},"page":"661-670","source":"Crossref","is-referenced-by-count":35,"title":["Probabilistic verification of Herman\u2019s self-stabilisation algorithm"],"prefix":"10.1145","volume":"24","author":[{"given":"Marta","family":"Kwiatkowska","sequence":"first","affiliation":[{"name":"Department of Computer Science, University of Oxford, Wolfson Building, Parks Road, OX1 3QD, Oxford, UK"}]},{"given":"Gethin","family":"Norman","sequence":"additional","affiliation":[{"name":"School of Computing Science, University of Glasgow, Glasgow, UK"}]},{"given":"David","family":"Parker","sequence":"additional","affiliation":[{"name":"Department of Computer Science, University of Oxford, Wolfson Building, Parks Road, OX1 3QD, Oxford, UK"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"crossref","unstructured":"Aziz A Singhal V Balarin F Brayton R Sangiovanni-Vincentelli A (1995) It usually works: The temporal logic of stochastic systems. In: Wolper P (ed) Proceedings of 7th Internatiol Conference on Computer Aided Verification (CAV\u201995) volume 939 of LNCS. Springer pp 155\u2013165","DOI":"10.1007\/3-540-60045-0_48"},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"crossref","unstructured":"Beauquier J Gradinariu M Johnen C (1999) Memory space requirements for self-stabilizing leader election protocols. In Proceedings of 18th ACM Symposium on principles of distributed computing (PODC\u201999). ACM pp 199\u2013208","DOI":"10.1145\/301308.301358"},{"key":"e_1_2_1_2_3_2","volume-title":"Principles of model checking","author":"Baier C","year":"2008"},{"key":"e_1_2_1_2_4_2","doi-asserted-by":"publisher","DOI":"10.1145\/361179.361202"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/6156.001.0001","volume-title":"Self-stabilization","author":"Dolev S","year":"2000"},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"crossref","unstructured":"Dhama A Theel O Crouzen P Hermanns H Wimmer R Becker B (2009) Dependability engineering of silent self-stabilizing systems. In: Proceedings of 11th International Symposium on stabilization safety and security of distributed systems volume 5873 of LNCS. Springer pp 238\u2013253","DOI":"10.1007\/978-3-642-05118-0_17"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00446-005-0142-7"},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"crossref","unstructured":"Herman T (1990) Probabilistic self-stabilization. Inform Process Lett. 35(2):63\u201367. ftp:\/\/ftp.math.uiowa.edu\/pub\/selfstab\/H90.html","DOI":"10.1016\/0020-0190(90)90107-9"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-010-0146-x"},{"key":"e_1_2_1_2_10_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF01211866"},{"key":"e_1_2_1_2_11_2","doi-asserted-by":"crossref","unstructured":"Hermanns H Wachter B Zhang L (2008) Probabilistic CEGAR. In: Gupta A Malik S (eds) Proceedings of 20th International Conference on Computer Aided Verification (CAV\u201908) volume 5123 of LNCS. Springer pp 162\u2013175","DOI":"10.1007\/978-3-540-70545-1_16"},{"key":"e_1_2_1_2_12_2","doi-asserted-by":"crossref","unstructured":"Israeli A Jalfon M (1990) Token management schemes and random walks yield self-stabilizating mutual exclusion. In: Proceedings of 9th ACM Symposium on principles of distributed computing (PODC\u201990). ACM pp 119\u2013131","DOI":"10.1145\/93385.93409"},{"key":"e_1_2_1_2_13_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-010-0097-6"},{"key":"e_1_2_1_2_14_2","doi-asserted-by":"crossref","unstructured":"Kiefer S Murawski A Ouaknine J Worrell J Zhang L (2011) On stabilization in Herman\u2019s algorithm. In: Aceto L Henzinger M Sgall J (eds) Proceedings on 38th International Colloquium on Automata Languages and Programming (ICALP\u201911) volume 6756 of LNCS. Springer pp 466\u2013477","DOI":"10.1007\/978-3-642-22012-8_37"},{"key":"e_1_2_1_2_15_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2005.10.030"},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"crossref","unstructured":"Kwiatkowska M Norman G Parker D (2007) Stochastic model checking. In: Bernardo M Hillston J (eds) Formal methods for the design of computer communication and software systems: performance evaluation (SFM\u201907) volume 4486 of LNCS. Springer pp 220\u2013270","DOI":"10.1007\/978-3-540-72522-0_6"},{"key":"e_1_2_1_2_17_2","doi-asserted-by":"crossref","unstructured":"Kwiatkowska M Norman G Parker D (2011) PRISM 4.0: Verification of probabilistic real-time systems. In: Gopalakrishnan G Qadeer S (eds) Proceedings of 23rd International Conference on Computer Aided Verification (CAV\u201911) volume 6806 of LNCS. Springer pp 585\u2013591","DOI":"10.1007\/978-3-642-22110-1_47"},{"key":"e_1_2_1_2_18_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4684-9455-6"},{"key":"e_1_2_1_2_19_2","volume-title":"Abstraction, refinement and proof for probabilistic systems","author":"McIver A","year":"2004"},{"issue":"2","key":"e_1_2_1_2_20_2","doi-asserted-by":"crossref","first-page":"79","DOI":"10.1016\/j.ipl.2004.12.013","article-title":"An elementary proof that Herman\u2019s ring is \u0398(N\n                  2)","volume":"94","author":"McIver A","year":"2005","journal-title":"Inform Process Lett."},{"key":"e_1_2_1_2_21_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2005.05.022"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-012-0227-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-012-0227-6\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-012-0227-6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T15:58:09Z","timestamp":1641484689000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-012-0227-6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,7]]},"references-count":21,"journal-issue":{"issue":"4-6","published-print":{"date-parts":[[2012,7]]}},"alternative-id":["10.1007\/s00165-012-0227-6"],"URL":"https:\/\/doi.org\/10.1007\/s00165-012-0227-6","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012,7]]}}}