{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T07:24:38Z","timestamp":1740122678673,"version":"3.37.3"},"reference-count":33,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2021,4,14]],"date-time":"2021-04-14T00:00:00Z","timestamp":1618358400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2021,4,14]],"date-time":"2021-04-14T00:00:00Z","timestamp":1618358400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"name":"Fonds de Recherche du Qu\u00e9bec - Nature et Technologies"},{"name":"European Research Council","award":["787367"],"award-info":[{"award-number":["787367"]}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2021,9]]},"abstract":"Abstract<\/jats:title>Population protocols are a well established model of computation by anonymous, identical finite-state agents. A protocol is well-specified if from every initial configuration, all fair executions of the protocol reach a common consensus. The central verification question for population protocols is the well-specification problem<\/jats:italic>: deciding if a given protocol is well-specified. Esparza et al. have recently shown that this problem is decidable, but with very high complexity: it is at least as hard as the Petri net reachability problem, which is -hard, and for which only algorithms of non-primitive recursive complexity are currently known. In this paper we introduce the class $${ WS}^3$$<\/jats:tex-math>\n \n \n WS<\/mml:mi>\n <\/mml:mrow>\n 3<\/mml:mn>\n <\/mml:msup>\n <\/mml:math><\/jats:alternatives><\/jats:inline-formula> of well-specified strongly-silent protocols and we prove that it is suitable for automatic verification. More precisely, we show that $${ WS}^3$$<\/jats:tex-math>\n \n \n WS<\/mml:mi>\n <\/mml:mrow>\n 3<\/mml:mn>\n <\/mml:msup>\n <\/mml:math><\/jats:alternatives><\/jats:inline-formula> has the same computational power as general well-specified protocols, and captures standard protocols from the literature. Moreover, we show that the membership and correctness problems for $${ WS}^3$$<\/jats:tex-math>\n \n \n WS<\/mml:mi>\n <\/mml:mrow>\n 3<\/mml:mn>\n <\/mml:msup>\n <\/mml:math><\/jats:alternatives><\/jats:inline-formula> reduce to solving boolean combinations of linear constraints over $${\\mathbb {N}}$$<\/jats:tex-math>\n N<\/mml:mi>\n <\/mml:math><\/jats:alternatives><\/jats:inline-formula>. This allowed us to develop the first software able to automatically prove correctness for all<\/jats:italic> of the infinitely many possible inputs.<\/jats:p>","DOI":"10.1007\/s10703-021-00367-3","type":"journal-article","created":{"date-parts":[[2021,4,14]],"date-time":"2021-04-14T00:02:37Z","timestamp":1618358557000},"page":"305-342","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Towards efficient verification of population protocols"],"prefix":"10.1007","volume":"57","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-2914-2734","authenticated-orcid":false,"given":"Michael","family":"Blondin","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9862-4919","authenticated-orcid":false,"given":"Javier","family":"Esparza","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5789-8091","authenticated-orcid":false,"given":"Stefan","family":"Jaax","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1334-9079","authenticated-orcid":false,"given":"Philipp J.","family":"Meyer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2021,4,14]]},"reference":[{"key":"367_CR1","doi-asserted-by":"publisher","unstructured":"Alistarh D, Gelashvili R, Vojnovic M (2015) Fast and exact majority in population protocols. In: ACM symposium on principles of distributed computing, PODC 2015, proceedings, ACM, pp 47\u201356. https:\/\/doi.org\/10.1145\/2767386.2767429","DOI":"10.1145\/2767386.2767429"},{"issue":"4","key":"367_CR2","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1007\/s00446-005-0138-3","volume":"18","author":"D Angluin","year":"2006","unstructured":"Angluin D, Aspnes J, Diamadi Z, Fischer MJ, Peralta R (2006a) Computation in networks of passively mobile finite-state sensors. Distrib Comput 18(4):235\u2013253. https:\/\/doi.org\/10.1007\/s00446-005-0138-3","journal-title":"Distrib Comput"},{"issue":"4","key":"367_CR3","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1007\/s00446-007-0040-2","volume":"20","author":"D Angluin","year":"2007","unstructured":"Angluin D, Aspnes J, Eisenstat D, Ruppert E (2007) The computational power of population protocols. Distrib Comput 20(4):279\u2013304. https:\/\/doi.org\/10.1007\/s00446-007-0040-2","journal-title":"Distrib Comput"},{"key":"367_CR4","doi-asserted-by":"publisher","unstructured":"Angluin D, Aspnes J, Diamadi Z, Fischer MJ, Peralta R (2004) Computation in networks of passively mobile finite-state sensors. In: Proceedings of 23rd annual ACM symposium on principles of distributed computing (PODC), pp 290\u2013299. https:\/\/doi.org\/10.1145\/1011767.1011810","DOI":"10.1145\/1011767.1011810"},{"key":"367_CR5","doi-asserted-by":"publisher","unstructured":"Angluin D, Aspnes J, Eisenstat D (2006b) Stably computable predicates are semilinear. In: Proceedings of 25th annual ACM symposium on principles of distributed computing (PODC), pp 292\u2013299. https:\/\/doi.org\/10.1145\/1146381.1146425","DOI":"10.1145\/1146381.1146425"},{"key":"367_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"516","DOI":"10.1007\/978-3-319-40229-1_35","volume-title":"Unbounded-thread program verification using thread-state equations IJCAR","author":"K Athanasiou","year":"2016","unstructured":"Athanasiou K, Liu P, Wahl T (2016) Unbounded-thread program verification using thread-state equations IJCAR, vol 9706. Lecture Notes in Computer Science. Springer, New York, pp 516\u2013531"},{"issue":"1","key":"367_CR7","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1016\/0304-3975(80)90037-7","volume":"11","author":"L Berman","year":"1980","unstructured":"Berman L (1980) The complexity of logical theories. Theor Comput Sci 11(1):71\u201377. https:\/\/doi.org\/10.1016\/0304-3975(80)90037-7","journal-title":"Theor Comput Sci"},{"key":"367_CR8","doi-asserted-by":"publisher","unstructured":"Blondin M, Esparza J, Jaax S (2018a) Large flocks of small birds: on the minimal size of population protocols. In: Proceedings of 35th symposium on theoretical aspects of computer science (STACS), pp 16:1\u201316:14. https:\/\/doi.org\/10.4230\/LIPIcs.STACS.2018.16","DOI":"10.4230\/LIPIcs.STACS.2018.16"},{"key":"367_CR9","doi-asserted-by":"publisher","unstructured":"Blondin M, Esparza J, Jaax S, Kucera A (2018b) Black ninjas in the dark: formal analysis of population protocols. In: Proceedings of the 33rd annual ACM\/IEEE symposium on logic in computer science, LICS 2018, Oxford, UK, July 09-12, 2018, pp 1\u201310. https:\/\/doi.org\/10.1145\/3209108.3209110","DOI":"10.1145\/3209108.3209110"},{"key":"367_CR10","doi-asserted-by":"crossref","unstructured":"Chatzigiannakis I, Michail O, Spirakis PG (2010) Algorithmic verification of population protocols. In: Proceedings of 12th international symposium on stabilization, safety, and security of distributed systems (SSS), pp 221\u2013235","DOI":"10.1007\/978-3-642-16023-3_19"},{"key":"367_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"16","DOI":"10.1007\/978-3-662-45174-8_2","volume-title":"Speed faults in computation by chemical reaction networks DISC","author":"H Chen","year":"2014","unstructured":"Chen H, Cummings R, Doty D, Soloveichik D (2014) Speed faults in computation by chemical reaction networks DISC, vol 8784. Lecture Notes in Computer Science. Springer, New York, pp 16\u201330"},{"key":"367_CR12","doi-asserted-by":"crossref","unstructured":"Cl\u00e9ment J, Delporte-Gallet C, Fauconnier H, Sighireanu M (2011) Guidelines for the verification of population protocols. In: ICDCS, IEEE computer society, pp 215\u2013224","DOI":"10.1109\/ICDCS.2011.36"},{"key":"367_CR13","first-page":"91","volume":"7","author":"D Cooper","year":"1972","unstructured":"Cooper D (1972) Theorem proving in arithmetic without multiplication. Mach Intell 7:91\u201399","journal-title":"Mach Intell"},{"key":"367_CR14","doi-asserted-by":"publisher","unstructured":"Czerwinski W, Lasota S, Lazic R, Leroux J, Mazowiecki F (2019) The reachability problem for petri nets is not elementary. In: Charikar M, Cohen E (eds) 51st annual ACM SIGACT symposium on theory of computing, STOC 2019, Phoenix, AZ, USA, June 23\u201326, 2019, Proceedings , pp 24\u201333. ACM. https:\/\/doi.org\/10.1145\/3313276.3316369","DOI":"10.1145\/3313276.3316369"},{"key":"367_CR15","doi-asserted-by":"crossref","unstructured":"de\u00a0Moura LM, Bj\u00f8rner N (2008) Z3: an efficient SMT solver. In: TACAS, Springer, Lecture Notes in Computer Science, vol 4963, pp 337\u2013340, z3 is available at https:\/\/github.com\/Z3Prover\/z3","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"367_CR16","doi-asserted-by":"publisher","unstructured":"Deng Y, Monin J (2009) Verifying self-stabilizing population protocols with Coq. In: Proceedings of 3rd IEEE international symposium on theoretical aspects of software engineering (TASE), pp 201\u2013208. https:\/\/doi.org\/10.1109\/TASE.2009.9","DOI":"10.1109\/TASE.2009.9"},{"key":"367_CR17","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511526558","volume-title":"Free Choice Petri Nets","author":"J Desel","year":"1995","unstructured":"Desel J, Esparza J (1995) Free Choice Petri Nets. Cambridge University Press, Cambridge"},{"issue":"6","key":"367_CR18","doi-asserted-by":"publisher","first-page":"447","DOI":"10.1007\/s002360050180","volume":"36","author":"S Dolev","year":"1999","unstructured":"Dolev S, Gouda MG, Schneider M (1999) Memory requirements for silent stabilization. Acta Inform 36(6):447\u2013462","journal-title":"Acta Inform"},{"issue":"2","key":"367_CR19","doi-asserted-by":"publisher","first-page":"159","DOI":"10.1023\/A:1008743212620","volume":"16","author":"J Esparza","year":"2000","unstructured":"Esparza J, Melzer S (2000) Verification of safety properties using integer programming: beyond the state equation. Formal Methods Syst Des 16(2):159\u2013189","journal-title":"Formal Methods Syst Des"},{"key":"367_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"603","DOI":"10.1007\/978-3-319-08867-9_40","volume-title":"An SMT-based approach to coverability analysis. CAV","author":"J Esparza","year":"2014","unstructured":"Esparza J, Ledesma-Garza R, Majumdar R, Meyer PJ, Nik\u0161i\u0107 F (2014) An SMT-based approach to coverability analysis. CAV, vol 8559. Lecture Notes in Computer Science. Springer, New York, pp 603\u2013619"},{"key":"367_CR21","unstructured":"Esparza J, Ganty P, Leroux J, Majumdar R (2015) Verification of population protocols. In: Proceedings of 26th international conference on concurrency theory (CONCUR), pp 470\u2013482"},{"key":"367_CR22","unstructured":"Esparza J, Ganty P, Leroux J, Majumdar R (2016) Model checking population protocols. In: FSTTCS, LIPIcs, vol\u00a065, pp 27:1\u201327:14"},{"key":"367_CR23","unstructured":"Fischer MJ, Rabin MO (1974) Super-exponential complexity of Presburger arithmetic. Technical report, MIT"},{"issue":"2","key":"367_CR24","doi-asserted-by":"publisher","first-page":"285","DOI":"10.2140\/pjm.1966.16.285","volume":"16","author":"S Ginsburg","year":"1966","unstructured":"Ginsburg S, Spanier E (1966) Semigroups, Presburger formulas, and languages. Pac J Math 16(2):285\u2013296","journal-title":"Pac J Math"},{"key":"367_CR25","doi-asserted-by":"publisher","first-page":"289","DOI":"10.1016\/0304-3975(88)90136-3","volume":"56","author":"E Gr\u00e4del","year":"1988","unstructured":"Gr\u00e4del E (1988) Subclasses of Presburger arithmetic and the polynomial-time hierarchy. Theor Comput Sci 56:289\u2013301","journal-title":"Theor Comput Sci"},{"key":"367_CR26","unstructured":"Hack MHT (1976) Decidability questions for Petri nets. Technical report 161, MIT"},{"issue":"22","key":"367_CR27","doi-asserted-by":"publisher","first-page":"2434","DOI":"10.1016\/j.tcs.2011.02.003","volume":"412","author":"O Michail","year":"2011","unstructured":"Michail O, Chatzigiannakis I, Spirakis PG (2011) Mediated population protocols. Theor Comput Sci 412(22):2434\u20132450","journal-title":"Theor Comput Sci"},{"key":"367_CR28","doi-asserted-by":"crossref","unstructured":"Michail O, Chatzigiannakis I, Spirakis PG (2012) Terminating population protocols via some minimal global knowledge assumptions. In: Stabilization, safety, and security of distributed systems\u201414th international symposium, SSS 2012, Toronto, Canada, October 1\u20134, 2012. Proceedings, pp 77\u201389","DOI":"10.1007\/978-3-642-33536-5_8"},{"issue":"1","key":"367_CR29","doi-asserted-by":"publisher","first-page":"94","DOI":"10.1145\/2678280","volume":"58","author":"S Navlakha","year":"2015","unstructured":"Navlakha S, Bar-Joseph Z (2015) Distributed information processing in biological and computational systems. Commun ACM 58(1):94\u2013102. https:\/\/doi.org\/10.1145\/2678280","journal-title":"Commun ACM"},{"key":"367_CR30","doi-asserted-by":"publisher","unstructured":"Pang J, Luo Z, Deng Y (2008) On automatic verification of self-stabilizing population protocols. In: Proceedings of 2nd IEEE\/IFIP international symposium on theoretical aspects of software engineering (TASE), pp 185\u2013192. https:\/\/doi.org\/10.1109\/TASE.2008.8","DOI":"10.1109\/TASE.2008.8"},{"key":"367_CR31","volume-title":"Computational complexity","author":"CH Papadimitriou","year":"2007","unstructured":"Papadimitriou CH (2007) Computational complexity. Academic Internet Publ, New York"},{"key":"367_CR32","volume-title":"Theory of linear and integer programming","author":"A Schrijver","year":"1986","unstructured":"Schrijver A (1986) Theory of linear and integer programming. Wiley, New York"},{"key":"367_CR33","doi-asserted-by":"publisher","unstructured":"Sun J, Liu Y, Dong JS, Pang J (2009) PAT: Towards flexible verification under fairness. In: Proceedings of 21st international conference on computer aided verification (CAV), pp 709\u2013714. https:\/\/doi.org\/10.1007\/978-3-642-02658-4_59","DOI":"10.1007\/978-3-642-02658-4_59"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-021-00367-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10703-021-00367-3\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-021-00367-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,12,1]],"date-time":"2021-12-01T12:11:18Z","timestamp":1638360678000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10703-021-00367-3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,4,14]]},"references-count":33,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2021,9]]}},"alternative-id":["367"],"URL":"https:\/\/doi.org\/10.1007\/s10703-021-00367-3","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"type":"print","value":"0925-9856"},{"type":"electronic","value":"1572-8102"}],"subject":[],"published":{"date-parts":[[2021,4,14]]},"assertion":[{"value":"26 October 2018","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"1 March 2021","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"14 April 2021","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}