{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:14:28Z","timestamp":1750306468479,"version":"3.41.0"},"publisher-location":"Cham","reference-count":31,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319587462"},{"type":"electronic","value":"9783319587479"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-58747-9_2","type":"book-chapter","created":{"date-parts":[[2017,5,5]],"date-time":"2017-05-05T01:14:05Z","timestamp":1493946845000},"page":"7-14","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Advances in Parameterized Verification of Population Protocols"],"prefix":"10.1007","author":[{"given":"Javier","family":"Esparza","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,5,6]]},"reference":[{"key":"2_CR1","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., Cerans, K., Jonsson, B., Tsay, Y.-K.: General decidability theorems for infinite-state systems. In: Proceedings of the 11th Annual IEEE Symposium on Logic in Computer Science, LICS 1996, pp. 313\u2013321. IEEE Computer Society (1996)","DOI":"10.1109\/LICS.1996.561359"},{"key":"2_CR2","doi-asserted-by":"crossref","unstructured":"Alistarh, D., Gelashvili, R., Vojnovic, M.: Fast and exact majority in population protocols. In: Proceedings of the ACM Symposium on Principles of Distributed Computing, PODC 2015, pp. 47\u201356. ACM (2015)","DOI":"10.1145\/2767386.2767429"},{"key":"2_CR3","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: PODC 2004, pp. 290\u2013299. ACM (2004)","DOI":"10.1145\/1011767.1011810"},{"issue":"4","key":"2_CR4","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."},{"key":"2_CR5","doi-asserted-by":"crossref","unstructured":"Angluin, D., Aspnes, J., Eisenstat, D.: Stably computable predicates are semilinear. In: PODC 2006, pp. 292\u2013299. ACM (2006)","DOI":"10.1145\/1146381.1146425"},{"issue":"3","key":"2_CR6","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1007\/s00446-008-0067-z","volume":"21","author":"D Angluin","year":"2008","unstructured":"Angluin, D., Aspnes, J., Eisenstat, D.: Fast computation by population protocols with a leader. Distrib. Comput. 21(3), 183\u2013199 (2008)","journal-title":"Distrib. Comput."},{"issue":"4","key":"2_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."},{"issue":"6","key":"2_CR8","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1016\/0020-0190(86)90071-2","volume":"22","author":"KR Apt","year":"1986","unstructured":"Apt, K.R., Kozen, D.C.: Limits for automatic verification of finite-state concurrent systems. Inf. Process. Lett. 22(6), 307\u2013309 (1986)","journal-title":"Inf. Process. Lett."},{"key":"2_CR9","doi-asserted-by":"crossref","unstructured":"Bloem, R., Jacobs, S., Khalimov, A., Konnov, I., Rubin, S., Veith, H., Widder, J.: Decidability of parameterized verification. In: Synthesis Lectures on Distributed Computing Theory. Morgan & Claypool Publishers (2015)","DOI":"10.1007\/978-3-031-02011-7"},{"key":"2_CR10","doi-asserted-by":"crossref","unstructured":"Blondin, M., Esparza, J., Jaax, S., Meyer, P.: Towards efficient verification of population protocols. CoRR, abs\/1703.04367 (2017)","DOI":"10.1145\/3087801.3087816"},{"key":"2_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1007\/978-3-642-16023-3_19","volume-title":"Stabilization, Safety, and Security of Distributed Systems","author":"I Chatzigiannakis","year":"2010","unstructured":"Chatzigiannakis, I., Michail, O., Spirakis, P.G.: Algorithmic Verification of Population Protocols. In: Dolev, S., Cobb, J., Fischer, M., Yung, M. (eds.) SSS 2010. LNCS, vol. 6366, pp. 221\u2013235. Springer, Heidelberg (2010). doi:10.1007\/978-3-642-16023-3_19"},{"key":"2_CR12","doi-asserted-by":"crossref","unstructured":"Clement, J., Delporte-Gallet, C., Fauconnier, H., Sighireanu, M.: Guidelines for the verification of population protocols. In: ICDCS 2011, pp. 215\u2013224 (2011)","DOI":"10.1109\/ICDCS.2011.36"},{"key":"2_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L Moura","year":"2008","unstructured":"Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). doi:10.1007\/978-3-540-78800-3_24"},{"key":"2_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"329","DOI":"10.1007\/978-3-540-77096-1_24","volume-title":"Principles of Distributed Systems","author":"C Delporte-Gallet","year":"2007","unstructured":"Delporte-Gallet, C., Fauconnier, H., Guerraoui, R., Ruppert, E.: Secretive birds: privacy in population protocols. In: Tovar, E., Tsigas, P., Fouchal, H. (eds.) OPODIS 2007. LNCS, vol. 4878, pp. 329\u2013342. Springer, Heidelberg (2007). doi:10.1007\/978-3-540-77096-1_24"},{"key":"2_CR15","doi-asserted-by":"crossref","unstructured":"Deng, Y., Monin, J.-F.: Verifying self-stabilizing population protocols with Coq. In: TASE 2009, pp. 201\u2013208. IEEE Computer Society (2009)","DOI":"10.1109\/TASE.2009.9"},{"issue":"1\u20132","key":"2_CR16","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1007\/BF03160228","volume":"6","author":"Z Diamadi","year":"2001","unstructured":"Diamadi, Z., Fischer, M.J.: A simple game for the study of trust in distributed systems. Wuhan Univ. J. Nat. Sci. 6(1\u20132), 72\u201382 (2001)","journal-title":"Wuhan Univ. J. Nat. Sci."},{"key":"2_CR17","unstructured":"Esparza, J.: Keeping a crowd safe: on the complexity of parameterized verification (invited talk). In: STACS. LIPIcs, vol. 25, pp. 1\u201310. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2014). Corrected version available in CoRR, abs\/1405.1841"},{"key":"2_CR18","unstructured":"Esparza, J., Ganty, P., Leroux, J., Majumdar, R.: Verification of population protocols. In: Proceedings of the 26th International Conference on Concurrency Theory (CONCUR), pp. 470\u2013482 (2015)"},{"key":"2_CR19","unstructured":"Esparza, J., Ganty, P., Leroux, J., Majumdar, R.: Model checking population protocols. In: FSTTCS. LIPIcs, vol. 65, pp. 27:1\u201327:14 (2016)"},{"issue":"2","key":"2_CR20","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 Inf. 54(2), 191\u2013215 (2017)","journal-title":"Acta Inf."},{"key":"2_CR21","doi-asserted-by":"crossref","unstructured":"Finkel, A., Schnoebelen, P.: Well-structured transition systems everywhere! Theor. Comput. Sci. 256(1\u20132), 63\u201392 (2001)","DOI":"10.1016\/S0304-3975(00)00102-X"},{"key":"2_CR22","doi-asserted-by":"crossref","unstructured":"Leroux, J.: The general vector addition system reachability problem by Presburger inductive invariants. In: LICS 2009, pp. 4\u201313. IEEE Computer Society (2009)","DOI":"10.1109\/LICS.2009.10"},{"key":"2_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"327","DOI":"10.1007\/978-3-642-23217-6_22","volume-title":"CONCUR 2011 \u2013 Concurrency Theory","author":"J Leroux","year":"2011","unstructured":"Leroux, J.: Vector addition system reversible reachability problem. In: Katoen, J.-P., K\u00f6nig, B. (eds.) CONCUR 2011. LNCS, vol. 6901, pp. 327\u2013341. Springer, Heidelberg (2011). doi:10.1007\/978-3-642-23217-6_22"},{"key":"2_CR24","doi-asserted-by":"crossref","unstructured":"Leroux, J.: Presburger vector addition systems. In: LICS 2013, pp. 23\u201332. IEEE Computer Society (2013)","DOI":"10.1109\/LICS.2013.7"},{"key":"2_CR25","doi-asserted-by":"crossref","unstructured":"Leroux, J.: Vector addition system reversible reachability problem. Log. Methods Comput. Sci. 9(1) (2013)","DOI":"10.2168\/LMCS-9(1:5)2013"},{"issue":"1","key":"2_CR26","doi-asserted-by":"publisher","first-page":"60","DOI":"10.1017\/S0305004100033193","volume":"54","author":"PAP Moran","year":"1958","unstructured":"Moran, P.A.P.: Random processes in genetics. Math. Proc. Camb. Philos. Soc. 54(1), 60\u201371 (1958)","journal-title":"Math. Proc. Camb. Philos. Soc."},{"issue":"1","key":"2_CR27","doi-asserted-by":"publisher","first-page":"94","DOI":"10.1145\/2678280","volume":"58","author":"S Navlakha","year":"2014","unstructured":"Navlakha, S., Bar-Joseph, Z.: Distributed information processing in biological and computational systems. Commun. ACM 58(1), 94\u2013102 (2014)","journal-title":"Commun. ACM"},{"key":"2_CR28","doi-asserted-by":"crossref","unstructured":"Pang, J., Luo, Z., Deng, Y.: On automatic verification of self-stabilizing population protocols. In: Proceedings of the 2nd IEEE\/IFIP International Symposium on Theoretical Aspects of Software Engineering (TASE), pp. 185\u2013192 (2008)","DOI":"10.1109\/TASE.2008.8"},{"issue":"1","key":"2_CR29","doi-asserted-by":"crossref","first-page":"4","DOI":"10.1145\/2893582.2893585","volume":"3","author":"S Schmitz","year":"2016","unstructured":"Schmitz, S.: The complexity of reachability in vector addition systems. SIGLOG News 3(1), 4\u201321 (2016)","journal-title":"SIGLOG News"},{"issue":"4","key":"2_CR30","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."},{"key":"2_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"709","DOI":"10.1007\/978-3-642-02658-4_59","volume-title":"Computer Aided Verification","author":"J Sun","year":"2009","unstructured":"Sun, J., Liu, Y., Dong, J.S., Pang, J.: PAT: towards flexible verification under fairness. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 709\u2013714. Springer, Heidelberg (2009). doi:10.1007\/978-3-642-02658-4_59"}],"container-title":["Lecture Notes in Computer Science","Computer Science \u2013 Theory and Applications"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-58747-9_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T05:45:12Z","timestamp":1750225512000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-58747-9_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319587462","9783319587479"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-58747-9_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]},"assertion":[{"value":"6 May 2017","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CSR","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Computer Science Symposium in Russia","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Kazan","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Russia","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2017","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"8 June 2017","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"12 June 2017","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"12","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"csr2017","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/logic.pdmi.ras.ru\/csr2017\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}