{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,29]],"date-time":"2025-11-29T07:55:55Z","timestamp":1764402955489,"version":"3.37.3"},"reference-count":49,"publisher":"Springer Science and Business Media LLC","issue":"1-2","license":[{"start":{"date-parts":[[2019,12,20]],"date-time":"2019-12-20T00:00:00Z","timestamp":1576800000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2019,12,20]],"date-time":"2019-12-20T00:00:00Z","timestamp":1576800000000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Acta Informatica"],"published-print":{"date-parts":[[2020,4]]},"DOI":"10.1007\/s00236-019-00361-7","type":"journal-article","created":{"date-parts":[[2019,12,20]],"date-time":"2019-12-20T12:02:56Z","timestamp":1576843376000},"page":"271-304","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["Parameterized synthesis of self-stabilizing protocols in symmetric networks"],"prefix":"10.1007","volume":"57","author":[{"given":"Nahal","family":"Mirzaie","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8877-6895","authenticated-orcid":false,"given":"Fathiyeh","family":"Faghih","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Swen","family":"Jacobs","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Borzoo","family":"Bonakdarpour","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2019,12,20]]},"reference":[{"key":"361_CR1","doi-asserted-by":"crossref","unstructured":"Alur, R., Raghothaman, M., Stergiou, C., Tripakis, S., Udupa, A.: Automatic completion of distributed protocols with symmetry. In International Conference on Computer Aided Verification, pp. 395\u2013412. Springer (2015)","DOI":"10.1007\/978-3-319-21668-3_23"},{"issue":"1","key":"361_CR2","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1145\/3061640.3061652","volume":"48","author":"R Alur","year":"2017","unstructured":"Alur, R., Tripakis, S.: Automatic synthesis of distributed protocols. SIGACT News 48(1), 55\u201390 (2017)","journal-title":"SIGACT News"},{"issue":"1","key":"361_CR3","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1145\/271510.271519","volume":"20","author":"PC Attie","year":"1998","unstructured":"Attie, P.C., Emerson, E.A.: Synthesis of concurrent systems with many similar processes. ACM Trans. Program. Lang. Syst. 20(1), 51\u2013115 (1998)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"361_CR4","first-page":"476","volume-title":"Lecture Notes in Computer Science","author":"Simon Au\u00dferlechner","year":"2015","unstructured":"Au\u00dferlechner, S., Jacobs, S., Khalimov, A.: Tight cutoffs for guarded protocols with fairness. In International Conference on Verification, Model Checking, and Abstract Interpretation, pp. 476\u2013494 (2016)"},{"key":"361_CR5","doi-asserted-by":"publisher","first-page":"315","DOI":"10.1007\/3-540-36577-X_23","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Samik Basu","year":"2003","unstructured":"Basu, S., Ramakrishnan, C.: Compositional analysis for verification of parameterized systems. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp. 315\u2013330 (2003)"},{"key":"361_CR6","unstructured":"Bingham, B., Greenstreet, M., Bingham, J.: Parameterized verification of deadlock freedom in symmetric cache coherence protocols. In International Conference on Formal Methods in Computer-Aided Design, pp. 186\u2013195 (2011)"},{"key":"361_CR7","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1007\/978-3-319-41528-4_9","volume-title":"Computer Aided Verification","author":"Roderick Bloem","year":"2016","unstructured":"Bloem, R., Braud-Santoni, N., Jacobs, S.: Synthesis of self-stabilising and byzantine-resilient distributed systems. In: Chaudhuri, S., Farzan, A. (eds.) Computer Aided Verification. Lecture Notes in Computer Science, vol. 9779, pp. 157\u2013176. Springer, Cham (2016)"},{"key":"361_CR8","doi-asserted-by":"publisher","first-page":"68","DOI":"10.4204\/EPTCS.157.9","volume":"157","author":"Roderick Bloem","year":"2014","unstructured":"Bloem, R., Jacobs, S., Khalimov, A.: Parameterized synthesis case study: AMBA AHB. In Workshop on Synthesis, volume 157 of EPTCS, pp. 68\u201383 (2014)","journal-title":"Electronic Proceedings in Theoretical Computer Science"},{"issue":"5","key":"361_CR9","doi-asserted-by":"publisher","first-page":"726","DOI":"10.1145\/265943.265960","volume":"19","author":"EM Clarke","year":"1997","unstructured":"Clarke, E.M., Grumberg, O., Jha, S.: Verifying parameterized networks. ACM Trans. Program. Lang. Syst. (TOPLAS) 19(5), 726\u2013750 (1997)","journal-title":"ACM Trans. Program. Lang. Syst. (TOPLAS)"},{"key":"361_CR10","first-page":"126","volume-title":"Lecture Notes in Computer Science","author":"Edmund Clarke","year":"2005","unstructured":"Clarke, E.M., Talupur, M., Veith, H.: Environment abstraction for parameterized verification. In: Emerson, E.A., Namjoshi, K.S. (eds.) Verification, Model Checking, and Abstract Interpretation. Lecture Notes in Computer Science, vol 3855, pp. 126\u2013141. Springer, Berlin, Heidelberg (2005)"},{"key":"361_CR11","doi-asserted-by":"publisher","first-page":"718","DOI":"10.1007\/978-3-642-31424-7_55","volume-title":"Computer Aided Verification","author":"Sylvain Conchon","year":"2012","unstructured":"Conchon, S., Goel, A., Krsti\u0107, S., Mebsout, A., Za\u00efdi, F.: Cubicle: A parallel SMT-based model checker for parameterized systems. In International Conference on Computer Aided Verification, pp. 718\u2013724 (2012)"},{"key":"361_CR12","doi-asserted-by":"crossref","unstructured":"Devismes, S., Tixeuil, S., Yamashita, M.: Weak vs. self vs. probabilistic stabilization. In: Proceedings of the 28th IEEE International Conference on Distributed Computing Systems (ICDCS), pp. 681\u2013688 (2008)","DOI":"10.1109\/ICDCS.2008.12"},{"issue":"11","key":"361_CR13","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"},{"issue":"1","key":"361_CR14","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1007\/BF01843566","volume":"1","author":"EW Dijkstra","year":"1986","unstructured":"Dijkstra, E.W.: A belated proof of self-stabilization. Distrib. Comput. 1(1), 5\u20136 (1986)","journal-title":"Distrib. Comput."},{"issue":"2","key":"361_CR15","doi-asserted-by":"publisher","first-page":"310","DOI":"10.1016\/j.jcss.2015.09.002","volume":"82","author":"D Dolev","year":"2016","unstructured":"Dolev, D., Heljanko, K., J\u00e4rvisalo, M., Korhonen, J., Lenzen, Ch., Rybicki, J., Suomela, J., Wieringa, S.: Synchronous counting and computational algorithm design. J. Comput. Syst. Sci. 82(2), 310\u2013332 (2016)","journal-title":"J. Comput. Syst. Sci."},{"key":"361_CR16","doi-asserted-by":"crossref","unstructured":"Ebnenasir, A., Farahat, A.: A lightweight method for automated design of convergence. In IPDPS, pp. 219\u2013230 (2011)","DOI":"10.1109\/IPDPS.2011.30"},{"key":"361_CR17","doi-asserted-by":"crossref","unstructured":"Ebnenasir, A., Klinkhamer, A.: Topology-specific synthesis of self-stabilizing parameterized systems with constant-space processes. IEEE Trans. Softw. Eng. (2019) (Available through Early Access)","DOI":"10.1109\/TSE.2019.2901485"},{"issue":"4","key":"361_CR18","doi-asserted-by":"publisher","first-page":"527","DOI":"10.1142\/S0129054103001881","volume":"14","author":"EA Emerson","year":"2003","unstructured":"Emerson, E.A., Namjoshi, K.S.: On reasoning about rings. Int. J. Found. Comput. Sci. 14(4), 527\u2013550 (2003)","journal-title":"Int. J. Found. Comput. Sci."},{"key":"361_CR19","doi-asserted-by":"publisher","first-page":"359","DOI":"10.1007\/3-540-45657-0_29","volume-title":"Computer Aided Verification","author":"Alessandro Cimatti","year":"2002","unstructured":"Cimatti et. al. A.: Nusmv 2: An opensource tool for symbolic model checking. In: Brinksma, E., Larsen, K.G. (eds.) Computer Aided Verification. Lecture Notes in Computer Science, vol. 2404, pp. 359\u2013364. Springer, Berlin, Heidelberg (2002)"},{"key":"361_CR20","first-page":"165","volume-title":"Lecture Notes in Computer Science","author":"Fathiyeh Faghih","year":"2014","unstructured":"Faghih, F., Bonakdarpour, B.: SMT-based synthesis of distributed self-stabilizing systems. In: Felber, P., Garg, V. (eds.) Stabilization, Safety, and Security of Distributed Systems. Lecture Notes in Computer Science, vol. 8756, pp. 165\u2013179. Springer, Cham (2014)"},{"issue":"3","key":"361_CR21","first-page":"21","volume":"10","author":"F Faghih","year":"2015","unstructured":"Faghih, F., Bonakdarpour, B.: SMT-based synthesis of distributed self-stabilizing systems. ACM Trans. Auton. Adapt. Syst. (TAAS) 10(3), 21 (2015)","journal-title":"ACM Trans. Auton. Adapt. Syst. (TAAS)"},{"key":"361_CR22","doi-asserted-by":"crossref","unstructured":"Faghih, F., Bonakdarpour, B.: ASSESS: A tool for automated synthesis of distributed self-stabilizing algorithms. In: SSS, pp. 219\u2013233 (2017)","DOI":"10.1007\/978-3-319-69084-1_15"},{"key":"361_CR23","doi-asserted-by":"publisher","first-page":"124","DOI":"10.1007\/978-3-319-39570-8_9","volume-title":"Formal Techniques for Distributed Objects, Components, and Systems","author":"Fathiyeh Faghih","year":"2016","unstructured":"Faghih, F., Bonakdarpour, B., Tixeuil, S., Kulkarni, S.: Specification-based synthesis of distributed self-stabilizing protocols. In: International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE), pp. 124\u2013141 (2016)"},{"key":"361_CR24","unstructured":"Faghih, F., Bonakdarpour, B., Tixeuil, S., Kulkarni, S.: Specification-based synthesis of distributed self-stabilizing protocols. In: Logical Methods in Computer Science (to appear)"},{"key":"361_CR25","unstructured":"Farahat, A.: Automated design of self-stabilization. PhD thesis, Michigan Technological University, (2012)"},{"key":"361_CR26","doi-asserted-by":"crossref","unstructured":"Farahat, A., Ebnenasir, A.: Local reasoning for global convergence of parameterized rings. In: International Conference on Distributed Computing Systems, pp. 496\u2013505 (2012)","DOI":"10.1109\/ICDCS.2012.66"},{"key":"361_CR27","first-page":"219","volume-title":"Lecture Notes in Computer Science","author":"Bernd Finkbeiner","year":"2012","unstructured":"Finkbeiner, B., Jacobs, S.: Lazy synthesis. In: Kuncak, V., Rybalchenko, A. (eds.) Verification, Model Checking, and Abstract Interpretation. Lecture Notes in Computer Science, vol. 7148, pp. 219\u2013234. Springer, Berlin, Heidelberg (2012)"},{"issue":"5\u20136","key":"361_CR28","doi-asserted-by":"publisher","first-page":"519","DOI":"10.1007\/s10009-012-0228-z","volume":"15","author":"B Finkbeiner","year":"2013","unstructured":"Finkbeiner, B., Schewe, S.: Bounded synthesis. Int. J. Softw. Tools Technol. Transf. (STTT) 15(5\u20136), 519\u2013539 (2013)","journal-title":"Int. J. Softw. Tools Technol. Transf. (STTT)"},{"key":"361_CR29","unstructured":"Gasc\u00f3n, A., Tiwari, A.: Synthesis of a simple self-stabilizing system (2014). arXiv preprint arXiv:1407.5392"},{"key":"361_CR30","first-page":"311","volume-title":"Lecture Notes in Computer Science","author":"Mohamed G. Gouda","year":"2009","unstructured":"Gouda, M. G., Acharya, H. B.: Nash equilibria in stabilizing systems. In: Guerraoui, R., Petit, F. (eds.) Stabilization, Safety, and Security of Distributed Systems. Lecture Notes in Computer Science, vol. 5873, pp. 311\u2013324. Springer, Berlin, Heidelberg (2009)"},{"key":"361_CR31","doi-asserted-by":"publisher","first-page":"338","DOI":"10.1007\/978-3-642-16901-4_23","volume-title":"Formal Methods and Software Engineering","author":"Youssef Hanna","year":"2010","unstructured":"Hanna, Y., Samuelson, D., Basu, S., Rajan, H.: Automating cut-off for multi-parameterized systems. In: International Conference on Formal Engineering Methods, pp. 338\u2013354 (2010)"},{"key":"361_CR32","volume-title":"Software Abstractions: Logic, Language, and Analysis","author":"D Jackson","year":"2012","unstructured":"Jackson, D.: Software Abstractions: Logic, Language, and Analysis. MIT Press, Cambridge (2012)"},{"key":"361_CR33","doi-asserted-by":"crossref","unstructured":"Jacobs, S., Bloem, R.: Parameterized synthesis. In: Logical Methods in Computer Science, vol. 10, No. 1 (2014)","DOI":"10.2168\/LMCS-10(1:12)2014"},{"key":"361_CR34","doi-asserted-by":"publisher","first-page":"211","DOI":"10.1007\/978-3-030-01090-4_13","volume-title":"Automated Technology for Verification and Analysis","author":"Swen Jacobs","year":"2018","unstructured":"Jacobs, S., Sakr, M.: A symbolic algorithm for lazy synthesis of eager strategies. In Automated Technology for Verification and Analysis (ATVA) (2018)"},{"key":"361_CR35","first-page":"247","volume-title":"Lecture Notes in Computer Science","author":"Swen Jacobs","year":"2017","unstructured":"Jacobs, S., Sakr, M.: Analyzing guarded protocols: Better cutoffs, more systems, more expressivity. In: Dillig, I., Palsberg, J. (eds.) Verification, Model Checking, and Abstract Interpretation. Lecture Notes in Computer Science, vol. 10747, pp. 247\u2013268. Springer, Cham (2018)"},{"key":"361_CR36","first-page":"108","volume-title":"Lecture Notes in Computer Science","author":"Ayrat Khalimov","year":"2013","unstructured":"Khalimov, A., Jacobs, S., Bloem, R.: Towards efficient parameterized synthesis. In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds.) Verification, Model Checking, and Abstract Interpretation. Lecture Notes in Computer Science, vol. 7737, pp. 108\u2013127. Springer, Berlin, Heidelberg (2013)"},{"key":"361_CR37","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1007\/978-3-642-40213-5_2","volume-title":"Fundamentals of Software Engineering","author":"Alex Klinkhamer","year":"2013","unstructured":"Klinkhamer, A., Ebnenasir, A.: On the complexity of adding convergence. In: Arbab, F., Sirjani, M. (eds.) Fundamentals of Software Engineering. Lecture Notes in Computer Science, vol. 8161, pp. 17\u201333. Springer, Berlin, Heidelberg (2013)"},{"key":"361_CR38","first-page":"163","volume-title":"Lecture Notes in Computer Science","author":"Alex P. Klinkhamer","year":"2013","unstructured":"Klinkhamer, A., Ebnenasir, A.: Verifying livelock freedom on parameterized rings and chains. In: Higashino, T., Katayama, Y., Masuzawa, T., Potop-Butucaru, M., Yamashita, M. (eds.) Stabilization, Safety, and Security of Distributed Systems. Lecture Notes in Computer Science, vol. 8255, pp. 163\u2013177. Springer, Cham (2013)"},{"key":"361_CR39","first-page":"252","volume-title":"Lecture Notes in Computer Science","author":"Alex Klinkhamer","year":"2014","unstructured":"Klinkhamer, A., Ebnenasir, A.: Synthesizing self-stabilization through superposition and backtracking. In: SSS, pp. 252\u2013267 (2014)"},{"issue":"11","key":"361_CR40","doi-asserted-by":"publisher","first-page":"3338","DOI":"10.1109\/TPDS.2016.2536023","volume":"27","author":"A Klinkhamer","year":"2016","unstructured":"Klinkhamer, A., Ebnenasir, A.: Shadow\/puppet synthesis: a stepwise method for the design of self-stabilization. IEEE Trans. Parallel Distrib. Syst. 27(11), 3338\u20133350 (2016)","journal-title":"IEEE Trans. Parallel Distrib. Syst."},{"key":"361_CR41","doi-asserted-by":"publisher","first-page":"100","DOI":"10.1007\/978-3-319-68972-2_7","volume-title":"Fundamentals of Software Engineering","author":"Alex P. Klinkhamer","year":"2017","unstructured":"Klinkhamer, A., Ebnenasir, A.: Synthesizing parameterized self-stabilizing rings with constant-space processes. In Fundamentals of Software Engineering (FSEN), pp. 100\u2013115 (2017)"},{"key":"361_CR42","unstructured":"Lazic, M., Konnov, I., Widder, J., Bloem, R.: Synthesis of distributed algorithms with parameterized threshold guards. In: On Principles of Distributed Systems (OPODIS) (2017)"},{"issue":"14","key":"361_CR43","doi-asserted-by":"publisher","first-page":"1336","DOI":"10.1016\/j.tcs.2008.12.022","volume":"410","author":"F Manne","year":"2009","unstructured":"Manne, F., Mjelde, M., Pilard, L., Tixeuil, S.: A new self-stabilizing maximal matching algorithm. Theor. Comput. Sci. 410(14), 1336\u20131345 (2009)","journal-title":"Theor. Comput. Sci."},{"key":"361_CR44","first-page":"179","volume-title":"Lecture Notes in Computer Science","author":"K. L. McMillan","year":"2001","unstructured":"McMillan, K.: Parameterized verification of the flash cache coherence protocol by compositional model checking. In: Advanced Research Working Conference on Correct Hardware Design and Verification Methods, pp. 179\u2013195 (2001)"},{"issue":"1","key":"361_CR45","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1145\/58564.59295","volume":"7","author":"Kerry Raymond","year":"1989","unstructured":"Raymond, Kerry: A tree-based algorithm for distributed mutual exclusion. ACM Trans. Comput. Syst. 7(1), 61\u201377 (1989)","journal-title":"ACM Trans. Comput. Syst."},{"key":"361_CR46","doi-asserted-by":"publisher","first-page":"256","DOI":"10.1007\/978-3-030-02146-7_13","volume-title":"Formal Aspects of Component Software","author":"Antti Siirtola","year":"2018","unstructured":"Siirtola, A., Heljanko, K.: Dynamic cut-off algorithm for parameterised refinement checking. In: International Conference on Formal Aspects of Component Software, pp. 256\u2013276 (2018)"},{"issue":"5\u20136","key":"361_CR47","doi-asserted-by":"publisher","first-page":"475","DOI":"10.1007\/s10009-012-0249-7","volume":"15","author":"A Solar-Lezama","year":"2013","unstructured":"Solar-Lezama, A.: Program sketching. STTT 15(5\u20136), 475\u2013495 (2013)","journal-title":"STTT"},{"issue":"2","key":"361_CR48","doi-asserted-by":"publisher","first-page":"242","DOI":"10.1109\/TEVC.2011.2112666","volume":"16","author":"T Weise","year":"2011","unstructured":"Weise, T., Tang, K.: Evolving distributed algorithms with genetic programming. IEEE Trans. Evol. Comput. 16(2), 242\u2013265 (2011)","journal-title":"IEEE Trans. Evol. Comput."},{"key":"361_CR49","doi-asserted-by":"crossref","unstructured":"Wolper, P., Lovinfosse, V.: Verifying properties of large sets of processes with network invariants. In: International Conference on Computer Aided Verification, pp. 68\u201380. Springer (1989)","DOI":"10.1007\/3-540-52148-8_6"}],"container-title":["Acta Informatica"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-019-00361-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00236-019-00361-7\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-019-00361-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,12,19]],"date-time":"2020-12-19T00:10:54Z","timestamp":1608336654000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s00236-019-00361-7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,12,20]]},"references-count":49,"journal-issue":{"issue":"1-2","published-print":{"date-parts":[[2020,4]]}},"alternative-id":["361"],"URL":"https:\/\/doi.org\/10.1007\/s00236-019-00361-7","relation":{},"ISSN":["0001-5903","1432-0525"],"issn-type":[{"type":"print","value":"0001-5903"},{"type":"electronic","value":"1432-0525"}],"subject":[],"published":{"date-parts":[[2019,12,20]]},"assertion":[{"value":"12 February 2019","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"6 December 2019","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"20 December 2019","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}