{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,1]],"date-time":"2026-10-01T00:19:15Z","timestamp":1790813955548,"version":"4.1.0"},"reference-count":49,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2021,3,24]],"date-time":"2021-03-24T00:00:00Z","timestamp":1616544000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2021,3,24]],"date-time":"2021-03-24T00:00:00Z","timestamp":1616544000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100000781","name":"European Research Council","doi-asserted-by":"publisher","award":["787367"],"award-info":[{"award-number":["787367"]}],"id":[{"id":"10.13039\/501100000781","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Distrib. Comput."],"published-print":{"date-parts":[[2021,4]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Population protocols (Angluin et al. in PODC, 2004) are a model of distributed computation in which indistinguishable, finite-state agents interact in pairs to decide if their initial configuration, i.e., the initial number of agents in each state, satisfies a given property. In a seminal paper Angluin et al. classified population protocols according to their communication mechanism, and conducted an exhaustive study of the expressive power of each class, that is, of the properties they can decide (Angluin et al. in Distrib Comput 20(4):279\u2013304, 2007). In this paper we study the correctness problem for population protocols, i.e., whether a given protocol decides a given property. A previous paper (Esparza et al. in Acta Inform 54(2):191\u2013215, 2017) has shown that the problem is decidable for the main population protocol model, but at least as hard as the reachability problem for Petri nets, which has recently been proved to have non-elementary complexity. Motivated by this result, we study the computational complexity of the correctness problem for all other classes introduced by Angluin et al., some of which are less powerful than the main model. Our main results show that for the class of observation models the complexity of the problem is much lower, ranging from <jats:inline-formula><jats:alternatives><jats:tex-math>$$\\varPi _2^p$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:msubsup>\n                    <mml:mi>\u03a0<\/mml:mi>\n                    <mml:mn>2<\/mml:mn>\n                    <mml:mi>p<\/mml:mi>\n                  <\/mml:msubsup>\n                <\/mml:math><\/jats:alternatives><\/jats:inline-formula> to .<\/jats:p>","DOI":"10.1007\/s00446-021-00390-x","type":"journal-article","created":{"date-parts":[[2021,3,24]],"date-time":"2021-03-24T09:02:52Z","timestamp":1616576572000},"page":"133-177","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["The complexity of verifying population protocols"],"prefix":"10.1007","volume":"34","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9862-4919","authenticated-orcid":false,"given":"Javier","family":"Esparza","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5789-8091","authenticated-orcid":false,"given":"Stefan","family":"Jaax","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6660-5673","authenticated-orcid":false,"given":"Mikhail","family":"Raskin","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1351-8824","authenticated-orcid":false,"given":"Chana","family":"Weil-Kennedy","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2021,3,24]]},"reference":[{"key":"390_CR1","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., Prasad Sistla, A., Talupur, M.: Model checking parameterized systems. In: Handbook of Model Checking, pp. 685\u2013725. Springer (2018)","DOI":"10.1007\/978-3-319-10575-8_21"},{"key":"390_CR2","doi-asserted-by":"crossref","unstructured":"Alistarh, D., Aspnes, J., Eisenstat, D., Gelashvili, R., Rivest, R.L.: Time-space trade-offs in population protocols. In: Proceedings of the Twenty-Eighth Annual ACM-SIAM Symposium on Discrete Algorithms (SODA), pp. 2560\u20132579 (2017)","DOI":"10.1137\/1.9781611974782.169"},{"key":"390_CR3","doi-asserted-by":"crossref","unstructured":"Alistarh, D., Aspnes, J., Gelashvili, R.: Space-optimal majority in population protocols. In: Proceedings of the Twenty-Ninth Annual ACM-SIAM Symposium on Discrete Algorithms (SODA), pp. 2221\u20132239 (2018)","DOI":"10.1137\/1.9781611975031.144"},{"issue":"3","key":"390_CR4","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1145\/3289137.3289150","volume":"49","author":"D Alistarh","year":"2018","unstructured":"Alistarh, D., Gelashvili, R.: Recent algorithmic advances in population protocols. SIGACT News 49(3), 63\u201373 (2018)","journal-title":"SIGACT News"},{"key":"390_CR5","doi-asserted-by":"crossref","unstructured":"Angluin, D., Aspnes, J., Diamadi, Z., Fischer, M.J., Peralta, R.: Computation in networks of passively mobile finite-state sensors. In Proceedings of the $$23^\\text{rd}$$ Annual ACM Symposium on Principles of Distributed Computing (PODC), pp. 290\u2013299 (2004)","DOI":"10.1145\/1011767.1011810"},{"issue":"4","key":"390_CR6","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, M.J., Peralta, R.: Computation in networks of passively mobile finite-state sensors. Distrib. Comput. 18(4), 235\u2013253 (2006)","journal-title":"Distrib. Comput."},{"issue":"4","key":"390_CR7","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.: The computational power of population protocols. Distrib. Comput. 20(4), 279\u2013304 (2007)","journal-title":"Distrib. Comput."},{"key":"390_CR8","doi-asserted-by":"crossref","unstructured":"Aspnes, J.: Clocked population protocols. In: PODC, pp. 431\u2013440. ACM (2017)","DOI":"10.1145\/3087801.3087836"},{"key":"390_CR9","doi-asserted-by":"crossref","unstructured":"Barrett, C.W., Tinelli, C.: Satisfiability modulo theories. In: Handbook of Model Checking, pp. 305\u2013343. Springer (2018)","DOI":"10.1007\/978-3-319-10575-8_11"},{"issue":"1","key":"390_CR10","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.: The complexity of logical theories. Theor. Comput. Sci. 11(1), 71\u201377 (1980)","journal-title":"Theor. Comput. Sci."},{"key":"390_CR11","unstructured":"Bertrand, N., Bouyer, P., Majumdar, A.: Reconfiguration and message losses in parameterized broadcast networks. In: CONCUR, volume 140 of LIPIcs, pp. 32:1\u201332:15. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2019)"},{"key":"390_CR12","doi-asserted-by":"crossref","unstructured":"Bloem, R., Jacobs, S., Khalimov, A., Konnov, I., Rubin, S., Veith, H., Widder, J.: Decidability of Parameterized Verification. Synthesis Lectures on Distributed Computing Theory. Morgan & Claypool Publishers (2015)","DOI":"10.2200\/S00658ED1V01Y201508DCT013"},{"key":"390_CR13","unstructured":"Blondin, M., Esparza, J., Genest, B., Helfrich, M., Jaax, S.: Succinct population protocols for presburger arithmetic. In: STACS, volume 154 of LIPIcs, pp. 40:1\u201340:15. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2020)"},{"key":"390_CR14","doi-asserted-by":"crossref","unstructured":"Blondin, M., Esparza, J., Helfrich, M., Kucera, A., Meyer, P.J.: Checking qualitative liveness properties of replicated systems with stochastic scheduling. In CAV (2), volume 12225 of Lecture Notes in Computer Science, pp. 372\u2013397. Springer (2020)","DOI":"10.1007\/978-3-030-53291-8_20"},{"key":"390_CR15","doi-asserted-by":"crossref","unstructured":"Blondin, M., Esparza, J., Jaax, S.: Peregrine: A tool for the analysis of population protocols. In: CAV (1), volume 10981 of Lecture Notes in Computer Science, pp. 604\u2013611. Springer (2018)","DOI":"10.1007\/978-3-319-96145-3_34"},{"key":"390_CR16","unstructured":"Blondin, M., Esparza, J., Jaax, S.: Expressive power of broadcast consensus protocols. In CONCUR, volume 140 of LIPIcs, pp. 31:1\u201331:16. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2019)"},{"key":"390_CR17","doi-asserted-by":"crossref","unstructured":"Blondin, M., Esparza, J., Jaax, S., Meyer, P.J.: Towards efficient verification of population protocols. In PODC, pages 423\u2013430. ACM (2017)","DOI":"10.1145\/3087801.3087816"},{"key":"390_CR18","unstructured":"Chatzigiannakis, I., Michail, O., Nikolaou, S., Pavlogiannis, A., Spirakis, P.G.: Passively mobile communicating logarithmic space machines. Technical report (2010)"},{"key":"390_CR19","doi-asserted-by":"crossref","unstructured":"Chatzigiannakis, I., Michail, O., Spirakis. P.G.: Algorithmic verification of population protocols. In: SSS \u201910, volume 6366 of LNCS, pp. 221\u2013235. Springer (2010)","DOI":"10.1007\/978-3-642-16023-3_19"},{"issue":"1 & 2","key":"390_CR20","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1016\/0304-3975(94)00231-7","volume":"147","author":"A Cheng","year":"1995","unstructured":"Cheng, A.: Esparza, J., Palsberg, J.: Complexity results for 1-safe nets. Theor. Comput. Sci. 147(1 & 2), 117\u2013136 (1995)","journal-title":"Theor. Comput. Sci."},{"key":"390_CR21","doi-asserted-by":"crossref","unstructured":"Clement, J., Delporte-Gallet, C., Fauconnier, H., Sighireanu, M.: Guidelines for the verification of population protocols. In: ICDCS \u201911, pp. 215\u2013224 (2011)","DOI":"10.1109\/ICDCS.2011.36"},{"key":"390_CR22","first-page":"91","volume":"7","author":"DC Cooper","year":"1972","unstructured":"Cooper, D.C.: Theorem proving in arithmetic without multiplication. Mach. Intell. 7, 91\u201399 (1972)","journal-title":"Mach. Intell."},{"issue":"2","key":"390_CR23","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1007\/s11047-015-9501-x","volume":"15","author":"R Cummings","year":"2016","unstructured":"Cummings, R., Doty, D., Soloveichik, D.: Probability 1 computation with chemical reaction networks. Natural Comput. 15(2), 245\u2013261 (2016)","journal-title":"Natural Comput."},{"key":"390_CR24","unstructured":"Czerwinski, W., Lasota, S., Lazic, R., Leroux, J., Mazowiecki, F.: The reachability problem for petri nets is not elementary. In: STOC, pp. 24\u201333. ACM (201)"},{"key":"390_CR25","unstructured":"Czerwinski, W., Lasota, S., Lazic, R., Leroux, J., Mazowiecki, F.: The reachability problem for petri nets is not elementary. In: Moses, C., Edith, C., (eds.) Proceedings of the 51st Annual ACM SIGACT Symposium on Theory of Computing, STOC 2019, Phoenix, AZ, USA, June 23-26, 2019, pp. 24\u201333. ACM (2019)"},{"issue":"3\u20134","key":"390_CR26","doi-asserted-by":"publisher","first-page":"287","DOI":"10.3233\/FI-2016-1315","volume":"143","author":"G Delzanno","year":"2016","unstructured":"Delzanno, G., Sangnier, A., Traverso, R.: Adding data registers to parameterized networks with broadcast. Fundam. Informaticae 143(3\u20134), 287\u2013316 (2016)","journal-title":"Fundam. Informaticae"},{"key":"390_CR27","unstructured":"Delzanno, G., Sangnier, A., Traverso, R., Zavattaro, G.: On the complexity of parameterized reachability in reconfigurable broadcast networks. In: FSTTCS, volume 18 of LIPIcs, pp. 289\u2013300. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2012)"},{"key":"390_CR28","first-page":"126","volume":"2018","author":"R Els\u00e4sser","year":"2018","unstructured":"Els\u00e4sser, R.: Radzik, T: Recent results in population protocols for exact majority and leader election. Bull. EATCS 2018, 126 (2018)","journal-title":"Bull. EATCS"},{"key":"390_CR29","doi-asserted-by":"crossref","unstructured":"Esparza, J.: Decidability and complexity of petri net problems-an introduction. In: P, N., volume 1491 of Lecture Notes in Computer Science, pp. 374\u2013428. Springer (1996)","DOI":"10.1007\/3-540-65306-6_20"},{"key":"390_CR30","unstructured":"Esparza, J.: Parameterized verification of crowds of anonymous processes. In: Dependable Software Systems Engineering, volume 45 of NATO Science for Peace and Security Series - D: Information and Communication Security, pp. 59\u201371. IOS Press (2016)"},{"key":"390_CR31","unstructured":"Esparza, J., Ganty, P., Leroux, J., Majumdar, R.: Model checking population protocols. In FSTTCS, volume 65 of LIPIcs, pp. 27:1\u201327:14. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2016)"},{"issue":"2","key":"390_CR32","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1007\/s00236-016-0272-3","volume":"54","author":"J Esparza","year":"2017","unstructured":"Esparza, J., Ganty, P., Leroux, J., Majumdar, R.: Verification of population protocols. Acta Informatica 54(2), 191\u2013215 (2017)","journal-title":"Acta Informatica"},{"key":"390_CR33","unstructured":"Esparza, J., Ganty, P., Majumdar, R., Weil-Kennedy, C.: Verification of immediate observation population protocols. In: CONCUR, volume 118 of LIPIcs, pp. 31:1\u201331:16. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2018)"},{"key":"390_CR34","doi-asserted-by":"crossref","unstructured":"Esparza, J., Raskin, M.A., Weil-Kennedy, C.: Parameterized analysis of immediate observation petri nets. In: Petri Nets, volume 11522 of Lecture Notes in Computer Science, pp. 365\u2013385. Springer (2019)","DOI":"10.1007\/978-3-030-21571-2_20"},{"key":"390_CR35","volume-title":"Super-exponential complexity of Presburger arithmetic","author":"MJ Fischer","year":"1974","unstructured":"Fischer, M.J., Rabin, M.O.: Super-exponential complexity of Presburger arithmetic. Technical report, MIT (1974)"},{"key":"390_CR36","unstructured":"Guerraoui, R., Ruppert, E.: Even small birds are unique: Population protocols with identifiers (2007)"},{"issue":"3","key":"390_CR37","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1145\/3242953.3242964","volume":"5","author":"C Haase","year":"2018","unstructured":"Haase, C.: A survival guide to presburger arithmetic. ACM SIGLOG News 5(3), 67\u201382 (2018)","journal-title":"ACM SIGLOG News"},{"key":"390_CR38","doi-asserted-by":"crossref","unstructured":"Leng\u00e1l, O., Lin, A.W., Majumdar, R., R\u00fcmmer, P.: Fair termination for parameterized probabilistic concurrent systems. In: TACAS (1), volume 10205 of Lecture Notes in Computer Science, pp. 499\u2013517 (2017)","DOI":"10.1007\/978-3-662-54577-5_29"},{"key":"390_CR39","doi-asserted-by":"crossref","unstructured":"Leroux, J.: Presburger vector addition systems. In: LICS, pp. 23\u201332. IEEE Computer Society (2013)","DOI":"10.1109\/LICS.2013.7"},{"key":"390_CR40","doi-asserted-by":"publisher","first-page":"1","DOI":"10.2168\/LMCS-9(1:5)2013","volume":"9","author":"J Leroux","year":"2013","unstructured":"Leroux, J.: Vector addition system reversible reachability problem. Log. Methods Comput. Sci. 9, 1 (2013)","journal-title":"Log. Methods Comput. Sci."},{"key":"390_CR41","doi-asserted-by":"crossref","unstructured":"Lin, A.W., R\u00fcmmer, P.: Liveness of randomised parameterised systems under arbitrary schedulers. In: CAV (2), volume 9780 of Lecture Notes in Computer Science, pp. 112\u2013133. Springer (2016)","DOI":"10.1007\/978-3-319-41540-6_7"},{"key":"390_CR42","unstructured":"Lipton, R.: The reachability problem is exponential-space hard. Technical Report 62, Department of Computer Science, Yale University, January (1976)"},{"issue":"2","key":"390_CR43","doi-asserted-by":"publisher","first-page":"639","DOI":"10.1007\/s11047-009-9152-x","volume":"10","author":"W Marwan","year":"2011","unstructured":"Marwan, W., Wagler, A., Weismantel, R.: Petri nets as a framework for the reconstruction and analysis of signal transduction pathways and regulatory networks. Nat. Comput. 10(2), 639\u2013654 (2011)","journal-title":"Nat. Comput."},{"issue":"22","key":"390_CR44","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, P.G.: Mediated population protocols. Theor. Comput. Sci. 412(22), 2434\u20132450 (2011)","journal-title":"Theor. Comput. Sci."},{"key":"390_CR45","doi-asserted-by":"crossref","unstructured":"Pang, J., Luo, Z., Deng, Y.: On automatic verification of self-stabilizing population protocols. In: TASE \u201908, pp. 185\u2013192. IEEE Computer Society (2008)","DOI":"10.1109\/TASE.2008.8"},{"key":"390_CR46","doi-asserted-by":"crossref","unstructured":"Piterman, N., Pnueli, A.: Temporal logic and fair discrete systems. In: Handbook of Model Checking, pp. 27\u201373. Springer (2018)","DOI":"10.1007\/978-3-319-10575-8_2"},{"issue":"4","key":"390_CR47","doi-asserted-by":"publisher","first-page":"615","DOI":"10.1007\/s11047-008-9067-y","volume":"7","author":"D Soloveichik","year":"2008","unstructured":"Soloveichik, D., Cook, M., Winfree, E., Bruck, J.: Computation with finite stochastic chemical reaction networks. Nat. Comput. 7(4), 615\u2013633 (2008)","journal-title":"Nat. Comput."},{"issue":"1","key":"390_CR48","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0304-3975(76)90061-X","volume":"3","author":"LJ Stockmeyer","year":"1976","unstructured":"Stockmeyer, L.J.: The polynomial-time hierarchy. Theor. Comput. Sci. 3(1), 1\u201322 (1976)","journal-title":"Theor. Comput. Sci."},{"key":"390_CR49","doi-asserted-by":"crossref","unstructured":"Sun, J., Liu, Y., Dong, J.S., Pang, J.: PAT: towards flexible verification under fairness. In: CAV \u201909, volume 5643 of LNCS, pp. 709\u2013714. Springer (2009)","DOI":"10.1007\/978-3-642-02658-4_59"}],"container-title":["Distributed Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00446-021-00390-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00446-021-00390-x\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00446-021-00390-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,3,29]],"date-time":"2021-03-29T18:05:03Z","timestamp":1617041103000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s00446-021-00390-x"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,3,24]]},"references-count":49,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2021,4]]}},"alternative-id":["390"],"URL":"https:\/\/doi.org\/10.1007\/s00446-021-00390-x","relation":{},"ISSN":["0178-2770","1432-0452"],"issn-type":[{"value":"0178-2770","type":"print"},{"value":"1432-0452","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,3,24]]},"assertion":[{"value":"13 December 2019","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"3 March 2021","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"24 March 2021","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}