{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,1]],"date-time":"2026-10-01T00:17:33Z","timestamp":1790813853558,"version":"4.1.0"},"reference-count":33,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2016,6,17]],"date-time":"2016-06-17T00:00:00Z","timestamp":1466121600000},"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":["Acta Informatica"],"published-print":{"date-parts":[[2017,3]]},"DOI":"10.1007\/s00236-016-0272-3","type":"journal-article","created":{"date-parts":[[2016,6,17]],"date-time":"2016-06-17T04:25:10Z","timestamp":1466137510000},"page":"191-215","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":33,"title":["Verification of population protocols"],"prefix":"10.1007","volume":"54","author":[{"given":"Javier","family":"Esparza","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Pierre","family":"Ganty","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"J\u00e9r\u00f4me","family":"Leroux","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Rupak","family":"Majumdar","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2016,6,17]]},"reference":[{"key":"272_CR1","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., Cerans, K., Jonsson, B., Tsay, Y.-K.: General decidability theorems for infinite-state systems. In: LICS\u201996: Proceedings of the 11th Annual IEEE Symposium on Logic in Computer Science, pp. 313\u2013321. IEEE Computer Society (1996)","DOI":"10.1109\/LICS.1996.561359"},{"key":"272_CR2","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\u201904, pp. 290\u2013299. ACM (2004)","DOI":"10.1145\/1011767.1011810"},{"issue":"4","key":"272_CR3","doi-asserted-by":"crossref","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":"272_CR4","doi-asserted-by":"crossref","unstructured":"Angluin, D., Aspnes, J., Eisenstat, D.: Fast computation by population protocols with a leader. In: DISC\u201906, Volume 4167 of LNCS, pp. 61\u201375. Springer, Berlin (2006)","DOI":"10.1007\/11864219_5"},{"key":"272_CR5","doi-asserted-by":"crossref","unstructured":"Angluin, D., Aspnes, J., Eisenstat, D.: Stably computable predicates are semilinear. In: PODC\u201906, pp. 292\u2013299. ACM (2006)","DOI":"10.1145\/1146381.1146425"},{"issue":"3","key":"272_CR6","doi-asserted-by":"crossref","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":"272_CR7","doi-asserted-by":"crossref","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":"272_CR8","doi-asserted-by":"crossref","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":"272_CR9","doi-asserted-by":"crossref","first-page":"15","DOI":"10.1016\/S1571-0661(05)80423-2","volume":"9","author":"Z Bouziane","year":"1997","unstructured":"Bouziane, Z., Finkel, A.: Cyclic petri net reachability sets are semi-linear effectively constructible. Electron. Notes Theor. Comput. Sci. 9, 15\u201324 (1997)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"272_CR10","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, Berlin (2010)","DOI":"10.1007\/978-3-642-16023-3_19"},{"key":"272_CR11","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":"272_CR12","doi-asserted-by":"crossref","unstructured":"Deng, Y., Monin, J.: Verifying self-stabilizing population protocols with coq. In: TASE\u201909, pp. 201\u2013208. IEEE Computer Society (2009)","DOI":"10.1109\/TASE.2009.9"},{"issue":"1\u20132","key":"272_CR13","doi-asserted-by":"crossref","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."},{"issue":"2","key":"272_CR14","doi-asserted-by":"crossref","first-page":"173","DOI":"10.1016\/0021-8693(69)90070-2","volume":"13","author":"S Eilenberg","year":"1969","unstructured":"Eilenberg, S., Sch\u00fctzenberger, M.P.: Rational sets in commutative monoids. J. Algebra 13(2), 173\u2013191 (1969)","journal-title":"J. Algebra"},{"key":"272_CR15","volume-title":"A Mathematical Introduction to Logic","author":"HB Enderton","year":"2001","unstructured":"Enderton, H.B.: A Mathematical Introduction to Logic. Academic Press, San Diego (2001)"},{"key":"272_CR16","doi-asserted-by":"crossref","unstructured":"Finkel, A., Leroux, J.: How to compose presburger-accelerations: Applications to broadcast protocols. In: FST TCS\u201902, Volume 2556 of Lecture Notes in Computer Science, pp. 145\u2013156. Springer, Berlin (2002)","DOI":"10.1007\/3-540-36206-1_14"},{"issue":"1\u20132","key":"272_CR17","doi-asserted-by":"crossref","first-page":"63","DOI":"10.1016\/S0304-3975(00)00102-X","volume":"256","author":"A Finkel","year":"2001","unstructured":"Finkel, A., Schnoebelen, P.: Well-structured transition systems everywhere!. Theor. Comput. Sci. 256(1\u20132), 63\u201392 (2001)","journal-title":"Theor. Comput. Sci."},{"key":"272_CR18","doi-asserted-by":"crossref","unstructured":"Fribourg, L., Ols\u00e9n, H.: Reductions of petri nets and unfolding of propositional logic programs. In: LOPSTR\u201996, Volume 1207 of Lecture Notes in Computer Science, pp. 187\u2013203. Springer, Berlin (1996)","DOI":"10.1007\/3-540-62718-9_11"},{"issue":"2","key":"272_CR19","doi-asserted-by":"crossref","first-page":"285","DOI":"10.2140\/pjm.1966.16.285","volume":"16","author":"S Ginsburg","year":"1966","unstructured":"Ginsburg, S., Spanier, E.H.: Semigroups, Presburger formulas, and languages. Pac. J. Math. 16(2), 285\u2013296 (1966)","journal-title":"Pac. J. Math."},{"key":"272_CR20","unstructured":"Hack, M.H.T.: Decidability questions for Petri nets. Technical Report 161, MIT (1976)"},{"key":"272_CR21","volume-title":"Congruences in Commutative Semigroups","author":"Y Hirshfeld","year":"1994","unstructured":"Hirshfeld, Y.: Congruences in Commutative Semigroups. LFCS, Department of Computer Science, University of Edinburgh, Edinburgh (1994)"},{"key":"272_CR22","doi-asserted-by":"crossref","unstructured":"Leroux, J.: The general vector addition system reachability problem by Presburger inductive invariants. In: LICS\u201909, pp. 4\u201313. IEEE Computer Society (2009)","DOI":"10.1109\/LICS.2009.10"},{"key":"272_CR23","doi-asserted-by":"crossref","unstructured":"Leroux, J.: Vector addition system reversible reachability problem. In: CONCUR\u201911, Volume 6901 of LNCS, pp. 327\u2013341. Springer, Berlin (2011)","DOI":"10.1007\/978-3-642-23217-6_22"},{"key":"272_CR24","unstructured":"Leroux, J.: Vector addition systems reachability problem (a simpler solution). In: Turing-100: The Alan Turing Centenary Conference, Volume\u00a010 of EPiC Series, pp. 214\u2013228. EasyChair (2012)"},{"key":"272_CR25","doi-asserted-by":"crossref","unstructured":"Leroux, J.: Presburger vector addition systems. In: LICS\u201913, pp. 23\u201332. IEEE Computer Society (2013)","DOI":"10.1109\/LICS.2013.7"},{"key":"272_CR26","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"},{"key":"272_CR27","doi-asserted-by":"crossref","unstructured":"Leroux, J., Schmitz, S.: Demystifying reachability in vector addition systems. In: LICS\u201915, pp. 56\u201367. IEEE Computer Society (2015)","DOI":"10.1109\/LICS.2015.16"},{"key":"272_CR28","doi-asserted-by":"crossref","unstructured":"Leroux, J., Sutre, G.: Flat counter automata almost everywhere!. In: Peled, D.A., Tsay, Y. (eds.), Automated Technology for Verification and Analysis, Third International Symposium, ATVA 2005, Taipei, Taiwan, October 4\u20137, 2005, Proceedings, Volume 3707 of Lecture Notes in Computer Science, pp. 489\u2013503. Springer, Berlin (2005)","DOI":"10.1007\/11562948_36"},{"key":"272_CR29","unstructured":"Lipton, R.: The Reachability Problem is Exponential-Space Hard. Technical Report\u00a062, Department of Computer Science, Yale University (1976)"},{"key":"272_CR30","doi-asserted-by":"crossref","unstructured":"Mayr, E.W.: An algorithm for the general petri net reachability problem. In: STOC\u201981, pp. 238\u2013246. ACM (1981)","DOI":"10.1145\/800076.802477"},{"issue":"1","key":"272_CR31","doi-asserted-by":"crossref","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":"272_CR32","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":"272_CR33","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, Berlin (2009)","DOI":"10.1007\/978-3-642-02658-4_59"}],"container-title":["Acta Informatica"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-016-0272-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00236-016-0272-3\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-016-0272-3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-016-0272-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,9]],"date-time":"2019-09-09T17:41:06Z","timestamp":1568050866000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s00236-016-0272-3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,6,17]]},"references-count":33,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2017,3]]}},"alternative-id":["272"],"URL":"https:\/\/doi.org\/10.1007\/s00236-016-0272-3","relation":{},"ISSN":["0001-5903","1432-0525"],"issn-type":[{"value":"0001-5903","type":"print"},{"value":"1432-0525","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016,6,17]]}}}