{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,14]],"date-time":"2025-06-14T17:22:01Z","timestamp":1749921721356,"version":"3.37.3"},"reference-count":31,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2021,11,8]],"date-time":"2021-11-08T00:00:00Z","timestamp":1636329600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2021,11,8]],"date-time":"2021-11-08T00:00:00Z","timestamp":1636329600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100008982","name":"National Science Foundation","doi-asserted-by":"publisher","award":["FMitF 1917979"],"award-info":[{"award-number":["FMitF 1917979"]}],"id":[{"id":"10.13039\/501100008982","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100000781","name":"European Research Council","doi-asserted-by":"publisher","award":["Advanced Grant 787914 FRAPPANT","Advanced Grant 787914 FRAPPANT"],"award-info":[{"award-number":["Advanced Grant 787914 FRAPPANT","Advanced Grant 787914 FRAPPANT"]}],"id":[{"id":"10.13039\/501100000781","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001659","name":"Deutsche Forschungsgemeinschaft","doi-asserted-by":"publisher","award":["DFG RTG 2236 UnRAVeL","DFG RTG 2236 UnRAVeL"],"award-info":[{"award-number":["DFG RTG 2236 UnRAVeL","DFG RTG 2236 UnRAVeL"]}],"id":[{"id":"10.13039\/501100001659","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Distrib. Comput."],"published-print":{"date-parts":[[2022,2]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Randomization is a key concept in distributed computing to tackle impossibility results. This also holds for <jats:italic>self-stabilization<\/jats:italic> in anonymous networks where coin flips are often used to break symmetry. Although the use of randomization in self-stabilizing algorithms is rather common, it is unclear what the optimal coin bias is so as to minimize the expected convergence time. This paper proposes a technique to automatically synthesize this optimal coin bias. Our algorithm is based on a parameter synthesis approach from the field of probabilistic model checking. It over- and under-approximates a given parameter region and iteratively refines the regions with minimal convergence time up to the desired accuracy. We describe the technique in detail and present a simple parallelization that gives an almost linear speed-up. We show the applicability of our technique to determine the optimal bias for the well-known Herman\u2019s self-stabilizing token ring algorithm. Our synthesis obtains that for small rings, a fair coin is optimal, whereas for larger rings a biased coin is optimal where the bias grows with the ring size. We also analyze a variant of Herman\u2019s algorithm that coincides with the original algorithm but deviates for biased coins. Finally, we show how using <jats:italic>speed reducers<\/jats:italic> in Herman\u2019s protocol improve the expected convergence time.\n<\/jats:p>","DOI":"10.1007\/s00446-021-00408-4","type":"journal-article","created":{"date-parts":[[2021,11,9]],"date-time":"2021-11-09T08:02:36Z","timestamp":1636444956000},"page":"37-57","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Synthesizing optimal bias in randomized self-stabilization"],"prefix":"10.1007","volume":"35","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-3810-4185","authenticated-orcid":false,"given":"Matthias","family":"Volk","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Borzoo","family":"Bonakdarpour","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Joost-Pieter","family":"Katoen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Saba","family":"Aflaki","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2021,11,8]]},"reference":[{"key":"408_CR1","doi-asserted-by":"crossref","unstructured":"Aflaki, S., Bonakdarpour, B., Tixeuil, S.: Automated analysis of impact of scheduling on performance of self-stabilizing protocols. In: SSS, LNCS, vol. 9212, pp. 156\u2013170. Springer, Berlin (2015)","DOI":"10.1007\/978-3-319-21741-3_11"},{"key":"408_CR2","doi-asserted-by":"crossref","unstructured":"Aflaki, S., Volk, M., Bonakdarpour, B., Katoen, J.P., Storjohann, A.: Automated fine tuning of probabilistic self-stabilizing algorithms. In: SRDS, pp. 94\u2013103. IEEE Computer Society, Washington, DC (2017)","DOI":"10.1109\/SRDS.2017.22"},{"key":"408_CR3","doi-asserted-by":"crossref","unstructured":"Angluin, D.: Local and global properties in networks of processors (extended abstract). In: STOC, pp. 82\u201393. ACM, New York (1980)","DOI":"10.1145\/800141.804655"},{"key":"408_CR4","volume-title":"Principles of Model Checking","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.P.: Principles of Model Checking. MIT Press, Cambridge (2008)"},{"key":"408_CR5","doi-asserted-by":"crossref","unstructured":"Bartocci, E., Grosu, R., Katsaros, P., Ramakrishnan, C.R., Smolka, S.A.: Model repair for probabilistic systems. In: TACAS, LNCS, vol. 6605, pp. 326\u2013340. Springer, Berlin (2011)","DOI":"10.1007\/978-3-642-19835-9_30"},{"issue":"4","key":"408_CR6","doi-asserted-by":"publisher","first-page":"824","DOI":"10.1145\/4221.214134","volume":"32","author":"G Bracha","year":"1985","unstructured":"Bracha, G., Toueg, S.: Asynchronous consensus and broadcast protocols. J. ACM 32(4), 824\u2013840 (1985)","journal-title":"J. ACM"},{"issue":"1","key":"408_CR7","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1016\/j.ic.2018.02.019","volume":"259","author":"G Chatzieleftheriou","year":"2018","unstructured":"Chatzieleftheriou, G., Katsaros, P.: Abstract model repair for probabilistic systems. Inf. Comput. 259(1), 142\u2013160 (2018)","journal-title":"Inf. Comput."},{"key":"408_CR8","doi-asserted-by":"crossref","unstructured":"Daws, C.: Symbolic and parametric model checking of discrete-time Markov chains. In: ICTAC, LNCS, vol. 3407, pp. 280\u2013294. Springer, Berlin (2004)","DOI":"10.1007\/978-3-540-31862-0_21"},{"key":"408_CR9","doi-asserted-by":"crossref","unstructured":"Dehnert, C., Junges, S., Jansen, N., Corzilius, F., Volk, M., Bruintjes, H., Katoen, J.P., \u00c1brah\u00e1m, E.: Prophesy: a probabilistic parameter synthesis tool. In: CAV (1), LNCS, vol. 9206, pp. 214\u2013231. Springer, Berlin (2015)","DOI":"10.1007\/978-3-319-21690-4_13"},{"key":"408_CR10","doi-asserted-by":"crossref","unstructured":"Dehnert, C., Junges, S., Katoen, J.P., Volk, M.: A storm is coming: a modern probabilistic model checker. In: CAV (2), LNCS, vol. 10427, pp. 592\u2013600. Springer, Berlin (2017)","DOI":"10.1007\/978-3-319-63390-9_31"},{"issue":"11","key":"408_CR11","doi-asserted-by":"publisher","first-page":"643","DOI":"10.1145\/361179.361202","volume":"17","author":"EW Dijkstra","year":"1974","unstructured":"Dijkstra, E.W.: Self-stabilizing systems in spite of distributed control. Commun. ACM 17(11), 643\u2013644 (1974)","journal-title":"Commun. ACM"},{"key":"408_CR12","doi-asserted-by":"publisher","DOI":"10.7551\/mitpress\/6156.001.0001","volume-title":"Self-stabilization","author":"S Dolev","year":"2000","unstructured":"Dolev, S.: Self-stabilization. MIT Press, Cambridge (2000)"},{"key":"408_CR13","doi-asserted-by":"crossref","unstructured":"Duchon, P., Hanusse, N., Tixeuil, S.: Optimal randomized self-stabilizing mutual exclusion on synchronous rings. In: DISC, LNCS, vol. 3274, pp. 216\u2013229. Springer, Berlin (2004)","DOI":"10.1007\/978-3-540-30186-8_16"},{"key":"408_CR14","doi-asserted-by":"crossref","unstructured":"Fallahi, N., Bonakdarpour, B.: How good is weak-stabilization? In: SSS, LNCS, vol. 8255, pp. 148\u2013162. Springer, Berlin (2013)","DOI":"10.1007\/978-3-319-03089-0_11"},{"key":"408_CR15","doi-asserted-by":"crossref","unstructured":"Fallahi, N., Bonakdarpour, B., Tixeuil, S.: Rigorous performance evaluation of self-stabilization using probabilistic model checking. In: SRDS, pp. 153\u2013162. IEEE Computer Society, Washington, DC (2013)","DOI":"10.1109\/SRDS.2013.24"},{"key":"408_CR16","doi-asserted-by":"crossref","unstructured":"Gordon, A.D., Henzinger, T.A., Nori, A.V., Rajamani, S.K.: Probabilistic programming. In: FOSE, pp. 167\u2013181. ACM, New York (2014)","DOI":"10.1145\/2593882.2593900"},{"key":"408_CR17","doi-asserted-by":"crossref","unstructured":"Hahn, E.M., Hartmanns, A., Hensel, C., Klauck, M., Klein, J., Kret\u00ednsk\u00fd, J., Parker, D., Quatmann, T., Ruijters, E., Steinmetz, M.: The 2019 comparison of tools for the analysis of quantitative formal models\u2014(QComp 2019 competition report). In: TACAS (3), LNCS, vol. 11429, pp. 69\u201392. Springer, Berlin (2019)","DOI":"10.1007\/978-3-030-17502-3_5"},{"issue":"1","key":"408_CR18","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/s10009-010-0146-x","volume":"13","author":"EM Hahn","year":"2011","unstructured":"Hahn, E.M., Hermanns, H., Zhang, L.: Probabilistic reachability for parametric Markov models. Int. J. Softw. Tools Technol. Transf. 13(1), 3\u201319 (2011)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"408_CR19","unstructured":"Hensel, C.: The probabilistic model checker Storm: symbolic methods for probabilistic model checking. Ph.D. thesis, RWTH Aachen University, Germany (2018)"},{"issue":"2","key":"408_CR20","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1016\/0020-0190(90)90107-9","volume":"35","author":"T Herman","year":"1990","unstructured":"Herman, T.: Probabilistic self-stabilization. Inf. Process. Lett. 35(2), 63\u201367 (1990)","journal-title":"Inf. Process. Lett."},{"issue":"6","key":"408_CR21","doi-asserted-by":"publisher","first-page":"651","DOI":"10.1007\/s10009-019-00536-0","volume":"21","author":"L Herrmann","year":"2019","unstructured":"Herrmann, L., K\u00fcttler, M., Stumpf, T., Baier, C., H\u00e4rtig, H., Kl\u00fcppelholz, S.: Configuration of inter-process communication with probabilistic model checking. STTT 21(6), 651\u2013666 (2019)","journal-title":"STTT"},{"key":"408_CR22","doi-asserted-by":"crossref","unstructured":"Hutschenreiter, L., Baier, C., Klein, J.: Parametric Markov chains: PCTL complexity and fraction-free Gaussian elimination. In: GandALF, EPTCS, vol. 256, pp. 16\u201330 (2017)","DOI":"10.4204\/EPTCS.256.2"},{"issue":"1","key":"408_CR23","doi-asserted-by":"publisher","first-page":"60","DOI":"10.1016\/0890-5401(90)90004-2","volume":"88","author":"A Itai","year":"1990","unstructured":"Itai, A., Rodeh, M.: Symmetry breaking in distributed networks. Inf. Comput. 88(1), 60\u201387 (1990)","journal-title":"Inf. Comput."},{"key":"408_CR24","unstructured":"Junges, S., \u00c1brah\u00e1m, E., Hensel, C., Jansen, N., Katoen, J.P., Quatmann, T., Volk, M.: Parameter synthesis for Markov models. CoRR arXiv:1903.07993 (2019)"},{"issue":"4\u20136","key":"408_CR25","doi-asserted-by":"publisher","first-page":"661","DOI":"10.1007\/s00165-012-0227-6","volume":"24","author":"MZ Kwiatkowska","year":"2012","unstructured":"Kwiatkowska, M.Z., Norman, G., Parker, D.: Probabilistic verification of Hermans self-stabilisation algorithm. Formal Asp. Comput. 24(4\u20136), 661\u2013670 (2012)","journal-title":"Formal Asp. Comput."},{"issue":"4","key":"408_CR26","doi-asserted-by":"publisher","first-page":"1036","DOI":"10.1137\/0215074","volume":"15","author":"M Luby","year":"1986","unstructured":"Luby, M.: A simple parallel algorithm for the maximal independent set problem. SIAM J. Comput. 15(4), 1036\u20131053 (1986)","journal-title":"SIAM J. Comput."},{"key":"408_CR27","doi-asserted-by":"crossref","unstructured":"Pathak, S., \u00c1brah\u00e1m, E., Jansen, N., Tacchella, A., Katoen, J.P.: A greedy approach for the efficient repair of stochastic models. In: NFM, LNCS, vol. 9058, pp. 295\u2013309. Springer, Berlin (2015)","DOI":"10.1007\/978-3-319-17524-9_21"},{"key":"408_CR28","doi-asserted-by":"publisher","DOI":"10.1002\/9780470316887","volume-title":"Markov Decision Processes: Discrete Stochastic Dynamic Programming. Wiley Series in Probability and Statistics","author":"ML Puterman","year":"1994","unstructured":"Puterman, M.L.: Markov Decision Processes: Discrete Stochastic Dynamic Programming. Wiley Series in Probability and Statistics. Wiley, New York (1994)"},{"key":"408_CR29","doi-asserted-by":"crossref","unstructured":"Quatmann, T., Dehnert, C., Jansen, N., Junges, S., Katoen, J.P.: Parameter synthesis for Markov models: faster than ever. In: ATVA, LNCS, vol. 9938, pp. 50\u201367 (2016)","DOI":"10.1007\/978-3-319-46520-3_4"},{"issue":"6","key":"408_CR30","doi-asserted-by":"publisher","first-page":"675","DOI":"10.1007\/s10009-016-0433-2","volume":"19","author":"T van Dijk","year":"2017","unstructured":"van Dijk, T., van de Pol, J.: Sylvan: multi-core framework for decision diagrams. Int. J. Softw. Tools Technol. Transf. 19(6), 675\u2013696 (2017)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"408_CR31","doi-asserted-by":"crossref","unstructured":"Zhu, L., Chen, J., Kulkarni, S.S.: Refinement of probabilistic stabilizing programs using genetic algorithms. In: SSS, LNCS, vol. 9212, pp. 217\u2013232. Springer, Berlin (2015)","DOI":"10.1007\/978-3-319-21741-3_15"}],"container-title":["Distributed Computing"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s00446-021-00408-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s00446-021-00408-4\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s00446-021-00408-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,2,27]],"date-time":"2022-02-27T08:03:47Z","timestamp":1645949027000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s00446-021-00408-4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,11,8]]},"references-count":31,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2022,2]]}},"alternative-id":["408"],"URL":"https:\/\/doi.org\/10.1007\/s00446-021-00408-4","relation":{},"ISSN":["0178-2770","1432-0452"],"issn-type":[{"type":"print","value":"0178-2770"},{"type":"electronic","value":"1432-0452"}],"subject":[],"published":{"date-parts":[[2021,11,8]]},"assertion":[{"value":"20 March 2020","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"14 September 2021","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"8 November 2021","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Declaration"}},{"value":"The authors declare that they have no conflict of interest.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Conflict of interest"}}]}}