{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,1]],"date-time":"2026-10-01T01:19:14Z","timestamp":1790817554910,"version":"4.1.0"},"publisher-location":"Cham","reference-count":65,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030532901","type":"print"},{"value":"9783030532918","type":"electronic"}],"license":[{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2020,7,14]],"date-time":"2020-07-14T00:00:00Z","timestamp":1594684800000},"content-version":"vor","delay-in-days":195,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2020]]},"DOI":"10.1007\/978-3-030-53291-8_20","type":"book-chapter","created":{"date-parts":[[2020,7,15]],"date-time":"2020-07-15T20:03:35Z","timestamp":1594843415000},"page":"372-397","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["Checking Qualitative Liveness Properties of Replicated Systems with Stochastic Scheduling"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-2914-2734","authenticated-orcid":false,"given":"Michael","family":"Blondin","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9862-4919","authenticated-orcid":false,"given":"Javier","family":"Esparza","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3191-8098","authenticated-orcid":false,"given":"Martin","family":"Helfrich","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6602-8028","authenticated-orcid":false,"given":"Anton\u00edn","family":"Ku\u010dera","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1334-9079","authenticated-orcid":false,"given":"Philipp J.","family":"Meyer","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2020,7,14]]},"reference":[{"issue":"2","key":"20_CR1","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1007\/s10009-011-0216-8","volume":"14","author":"PA Abdulla","year":"2012","unstructured":"Abdulla, P.A.: Regular model checking. Int. J. Softw. Tools Technol. Transf. 14(2), 109\u2013118 (2012). \nhttps:\/\/doi.org\/10.1007\/s10009-011-0216-8","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"20_CR2","doi-asserted-by":"publisher","unstructured":"Abdulla, P.A., Cerans, K., Jonsson, B., Tsay, Y.: General decidability theorems for infinite-state systems. In: Proceedings of the 11th Annual IEEE Symposium on Logic in Computer Science, LICS 1996, New Brunswick, New Jersey, USA, 27\u201330 July 1996, pp. 313\u2013321. IEEE Computer Society (1996). \nhttps:\/\/doi.org\/10.1109\/LICS.1996.561359","DOI":"10.1109\/LICS.1996.561359"},{"key":"20_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"721","DOI":"10.1007\/978-3-540-71209-1_56","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"PA Abdulla","year":"2007","unstructured":"Abdulla, P.A., Delzanno, G., Henda, N.B., Rezine, A.: Regular model checking without transducers (on efficient verification of parameterized systems). In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 721\u2013736. Springer, Heidelberg (2007). \nhttps:\/\/doi.org\/10.1007\/978-3-540-71209-1_56"},{"issue":"3","key":"20_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). \nhttps:\/\/doi.org\/10.1145\/3289137.3289150","journal-title":"SIGACT News"},{"key":"20_CR5","doi-asserted-by":"publisher","unstructured":"Alistarh, D., Gelashvili, R., Vojnovic, M.: Fast and exact majority in population protocols. In: Georgiou, C., Spirakis, P.G. (eds.) Proceedings of the 34th ACM Symposium on Principles of Distributed Computing, PODC 2015, Donostia-San Sebasti\u00e1n, Spain, 21\u201323 July 2015, pp. 47\u201356. ACM (2015). \nhttps:\/\/doi.org\/10.1145\/2767386.2767429","DOI":"10.1145\/2767386.2767429"},{"key":"20_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"375","DOI":"10.1007\/978-3-662-47666-6_30","volume-title":"Automata, Languages, and Programming","author":"B Aminof","year":"2015","unstructured":"Aminof, B., Rubin, S., Zuleger, F., Spegni, F.: Liveness of parameterized timed networks. In: Halld\u00f3rsson, M.M., Iwama, K., Kobayashi, N., Speckmann, B. (eds.) ICALP 2015, Part II. LNCS, vol. 9135, pp. 375\u2013387. Springer, Heidelberg (2015). \nhttps:\/\/doi.org\/10.1007\/978-3-662-47666-6_30"},{"issue":"2","key":"20_CR7","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1016\/0890-5401(87)90052-6","volume":"75","author":"D Angluin","year":"1987","unstructured":"Angluin, D.: Learning regular sets from queries and counterexamples. Inf. Comput. 75(2), 87\u2013106 (1987). \nhttps:\/\/doi.org\/10.1016\/0890-5401(87)90052-6","journal-title":"Inf. Comput."},{"key":"20_CR8","doi-asserted-by":"publisher","unstructured":"Angluin, D., Aspnes, J., Diamadi, Z., Fischer, M.J., Peralta, R.: Computation in networks of passively mobile finite-state sensors. In: Chaudhuri, S., Kutten, S. (eds.) Proceedings of the 23rd Annual ACM Symposium on Principles of Distributed Computing, PODC 2004, St. John\u2019s, Newfoundland, Canada, 25\u201328 July 2004, pp. 290\u2013299. ACM (2004). \nhttps:\/\/doi.org\/10.1145\/1011767.1011810","DOI":"10.1145\/1011767.1011810"},{"issue":"4","key":"20_CR9","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). \nhttps:\/\/doi.org\/10.1007\/s00446-005-0138-3","journal-title":"Distrib. Comput."},{"issue":"4","key":"20_CR10","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). \nhttps:\/\/doi.org\/10.1007\/s00446-007-0040-2","journal-title":"Distrib. Comput."},{"key":"20_CR11","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"516","DOI":"10.1007\/978-3-319-40229-1_35","volume-title":"Automated Reasoning","author":"K Athanasiou","year":"2016","unstructured":"Athanasiou, K., Liu, P., Wahl, T.: Unbounded-thread program verification using thread-state equations. In: Olivetti, N., Tiwari, A. (eds.) IJCAR 2016. LNCS (LNAI), vol. 9706, pp. 516\u2013531. Springer, Cham (2016). \nhttps:\/\/doi.org\/10.1007\/978-3-319-40229-1_35"},{"key":"20_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"479","DOI":"10.1007\/978-3-319-21690-4_31","volume-title":"Computer Aided Verification","author":"T Babiak","year":"2015","unstructured":"Babiak, T., et al.: The Hanoi omega-automata format. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015, Part I. LNCS, vol. 9206, pp. 479\u2013486. Springer, Cham (2015). \nhttps:\/\/doi.org\/10.1007\/978-3-319-21690-4_31"},{"key":"20_CR13","volume-title":"Principles of Model Checking","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.: Principles of Model Checking. MIT Press, Cambridge (2008)"},{"key":"20_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"64","DOI":"10.1007\/978-3-642-02658-4_9","volume-title":"Computer Aided Verification","author":"G Basler","year":"2009","unstructured":"Basler, G., Mazzucchi, M., Wahl, T., Kroening, D.: Symbolic counter abstraction for concurrent software. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 64\u201378. Springer, Heidelberg (2009). \nhttps:\/\/doi.org\/10.1007\/978-3-642-02658-4_9"},{"key":"20_CR15","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 complexitiy of logical theories. Theoret. Comput. Sci. 11, 71\u201377 (1980). \nhttps:\/\/doi.org\/10.1016\/0304-3975(80)90037-7","journal-title":"Theoret. Comput. Sci."},{"key":"20_CR16","doi-asserted-by":"publisher","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). \nhttps:\/\/doi.org\/10.2200\/S00658ED1V01Y201508DCT013","DOI":"10.2200\/S00658ED1V01Y201508DCT013"},{"key":"20_CR17","doi-asserted-by":"publisher","unstructured":"Blondin, M., Esparza, J., Genest, B., Helfrich, M., Jaax, S.: Succinct population protocols for presburger arithmetic. In: Proceedings of 37th International Symposium on Theoretical Aspects of Computer Science, STACS 2020, 10\u201313 March 2020, Montpellier, France. LIPIcs, vol. 154, pp. 40:1\u201340:15. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2020). \nhttps:\/\/doi.org\/10.4230\/LIPIcs.STACS.2020.40","DOI":"10.4230\/LIPIcs.STACS.2020.40"},{"key":"20_CR18","doi-asserted-by":"publisher","unstructured":"Blondin, M., Esparza, J., Helfrich, M., Ku\u010dera, A., Meyer, P.J.: Artifact evaluation VM and instructions to generate experimental results for the CAV20 paper: checking Qualitative Liveness Properties of Replicated Systems with Stochastic Scheduling. figshare:12295982 (2020). \nhttps:\/\/doi.org\/10.6084\/m9.figshare.12295982.v2","DOI":"10.6084\/m9.figshare.12295982.v2"},{"key":"20_CR19","unstructured":"Blondin, M., Esparza, J., Helfrich, M., Ku\u010dera, A., Meyer, P.J.: Checking qualitative liveness properties of replicated systems with stochastic scheduling. \narXiv:2005.03555\n\n [cs.LO] (2020). \nhttps:\/\/arxiv.org\/abs\/2005.03555"},{"key":"20_CR20","doi-asserted-by":"publisher","unstructured":"Blondin, M., Esparza, J., Jaax, S.: Large flocks of small birds: on the minimal size of population protocols. In: Proceedings of 35th Symposium on Theoretical Aspects of Computer Science, STACS 2018, 28 February - 3 March 2018, Caen, France. LIPIcs, vol. 96, pp. 16:1\u201316:14. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2018). \nhttps:\/\/doi.org\/10.4230\/LIPIcs.STACS.2018.16","DOI":"10.4230\/LIPIcs.STACS.2018.16"},{"key":"20_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"604","DOI":"10.1007\/978-3-319-96145-3_34","volume-title":"Computer Aided Verification","author":"M Blondin","year":"2018","unstructured":"Blondin, M., Esparza, J., Jaax, S.: Peregrine: a tool for the analysis of population protocols. In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018, Part I. LNCS, vol. 10981, pp. 604\u2013611. Springer, Cham (2018). \nhttps:\/\/doi.org\/10.1007\/978-3-319-96145-3_34"},{"key":"20_CR22","doi-asserted-by":"publisher","unstructured":"Blondin, M., Esparza, J., Jaax, S., Meyer, P.J.: Towards efficient verification of population protocols. In: Schiller, E.M., Schwarzmann, A.A. (eds.) Proceedings of 36th ACM Symposium on Principles of Distributed Computing, PODC 2017, Washington, DC, USA, 25\u201327 July 2017, pp. 423\u2013430. ACM (2017). \nhttps:\/\/doi.org\/10.1145\/3087801.3087816","DOI":"10.1145\/3087801.3087816"},{"key":"20_CR23","doi-asserted-by":"publisher","unstructured":"Blondin, M., Esparza, J., Ku\u010dera, A.: Automatic analysis of expected termination time for population protocols. In: Schewe, S., Zhang, L. (eds.) Proceedings of 29th International Conference on Concurrency Theory, CONCUR 2018, 4\u20137 September 2018, Beijing, China. LIPIcs, vol. 118, pp. 33:1\u201333:16. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2018). \nhttps:\/\/doi.org\/10.4230\/LIPIcs.CONCUR.2018.33","DOI":"10.4230\/LIPIcs.CONCUR.2018.33"},{"issue":"3","key":"20_CR24","doi-asserted-by":"publisher","first-page":"24:1","DOI":"10.1145\/3105908","volume":"18","author":"M Blondin","year":"2017","unstructured":"Blondin, M., Finkel, A., Haase, C., Haddad, S.: The logical view on continuous petri nets. ACM Trans. Comput. Log. (TOCL) 18(3), 24:1\u201324:28 (2017). \nhttps:\/\/doi.org\/10.1145\/3105908","journal-title":"ACM Trans. Comput. Log. (TOCL)"},{"key":"20_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"403","DOI":"10.1007\/10722167_31","volume-title":"Computer Aided Verification","author":"A Bouajjani","year":"2000","unstructured":"Bouajjani, A., Jonsson, B., Nilsson, M., Touili, T.: Regular model checking. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 403\u2013418. Springer, Heidelberg (2000). \nhttps:\/\/doi.org\/10.1007\/10722167_31"},{"issue":"1","key":"20_CR26","doi-asserted-by":"publisher","first-page":"13","DOI":"10.1016\/0890-5401(89)90026-6","volume":"81","author":"MC Browne","year":"1989","unstructured":"Browne, M.C., Clarke, E.M., Grumberg, O.: Reasoning about networks with many identical finite state processes. Inf. Comput. 81(1), 13\u201331 (1989). \nhttps:\/\/doi.org\/10.1016\/0890-5401(89)90026-6","journal-title":"Inf. Comput."},{"issue":"1","key":"20_CR27","doi-asserted-by":"publisher","first-page":"656","DOI":"10.1038\/srep00656","volume":"2","author":"L Cardelli","year":"2012","unstructured":"Cardelli, L., Csik\u00e1sz-Nagy, A.: The cell cycle switch computes approximate majority. Sci. Rep. 2(1), 656 (2012). \nhttps:\/\/doi.org\/10.1038\/srep00656","journal-title":"Sci. Rep."},{"key":"20_CR28","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). \nhttps:\/\/doi.org\/10.1007\/978-3-642-16023-3_19"},{"key":"20_CR29","doi-asserted-by":"publisher","unstructured":"Chen, Y., Hong, C., Lin, A.W., R\u00fcmmer, P.: Learning to prove safety over parameterised concurrent systems. In: Stewart, D., Weissenbacher, G. (eds.) Proceedings of 17th International Conference on Formal Methods in Computer Aided Design, FMCAD 2017, Vienna, Austria, 2\u20136 October 2017, pp. 76\u201383. IEEE (2017). \nhttps:\/\/doi.org\/10.23919\/FMCAD.2017.8102244","DOI":"10.23919\/FMCAD.2017.8102244"},{"key":"20_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"276","DOI":"10.1007\/978-3-540-28644-8_18","volume-title":"CONCUR 2004 - Concurrency Theory","author":"E Clarke","year":"2004","unstructured":"Clarke, E., Talupur, M., Touili, T., Veith, H.: Verification by network decomposition. In: Gardner, P., Yoshida, N. (eds.) CONCUR 2004. LNCS, vol. 3170, pp. 276\u2013291. Springer, Heidelberg (2004). \nhttps:\/\/doi.org\/10.1007\/978-3-540-28644-8_18"},{"key":"20_CR31","doi-asserted-by":"publisher","unstructured":"Cl\u00e9ment, J., Delporte-Gallet, C., Fauconnier, H., Sighireanu, M.: Guidelines for the verification of population protocols. In: Proceedings of 31st International Conference on Distributed Computing Systems, ICDCS 2011, Minneapolis, Minnesota, USA, 20\u201324 June 2011, pp. 215\u2013224. IEEE Computer Society (2011). \nhttps:\/\/doi.org\/10.1109\/ICDCS.2011.36","DOI":"10.1109\/ICDCS.2011.36"},{"key":"20_CR32","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."},{"key":"20_CR33","doi-asserted-by":"publisher","unstructured":"Czerwinski, W., Lasota, S., Lazic, R., Leroux, J., Mazowiecki, F.: The reachability problem for petri nets is not elementary. In: Charikar, M., Cohen, E. (eds.) Proceedings of 51st Annual ACM SIGACT Symposium on Theory of Computing, STOC 2019, Phoenix, AZ, USA, 23\u201326 June 2019, pp. 24\u201333. ACM (2019). \nhttps:\/\/doi.org\/10.1145\/3313276.3316369","DOI":"10.1145\/3313276.3316369"},{"issue":"4","key":"20_CR34","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). \nhttps:\/\/doi.org\/10.1142\/S0129054103001881","journal-title":"Int. J. Found. Comput. Sci."},{"key":"20_CR35","doi-asserted-by":"publisher","unstructured":"Esparza, J., Ganty, P., Leroux, J., Majumdar, R.: Model checking population protocols. In: Lal, A., Akshay, S., Saurabh, S., Sen, S. (eds.) Proceedings of 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2016, Chennai, India, 13\u201315 December 2016. LIPIcs, vol. 65, pp. 27:1\u201327:14. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2016). \nhttps:\/\/doi.org\/10.4230\/LIPIcs.FSTTCS.2016.27","DOI":"10.4230\/LIPIcs.FSTTCS.2016.27"},{"issue":"2","key":"20_CR36","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). \nhttps:\/\/doi.org\/10.1007\/s00236-016-0272-3","journal-title":"Acta Inf."},{"key":"20_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"603","DOI":"10.1007\/978-3-319-08867-9_40","volume-title":"Computer Aided Verification","author":"J Esparza","year":"2014","unstructured":"Esparza, J., Ledesma-Garza, R., Majumdar, R., Meyer, P., Niksic, F.: An SMT-based approach to coverability analysis. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 603\u2013619. Springer, Cham (2014). \nhttps:\/\/doi.org\/10.1007\/978-3-319-08867-9_40"},{"key":"20_CR38","doi-asserted-by":"crossref","unstructured":"Esparza, J., Meyer, P.J.: An SMT-based approach to fair termination analysis. In: Kaivola, R., Wahl, T. (eds.) Proceedings of 15th International Conference on Formal Methods in Computer-Aided Design, FMCAD 2015, Austin, Texas, USA, 27\u201330 September 2015, pp. 49\u201356. IEEE (2015)","DOI":"10.1109\/FMCAD.2015.7542252"},{"issue":"1\u20132","key":"20_CR39","doi-asserted-by":"publisher","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!. Theoret. Comput. Sci. 256(1\u20132), 63\u201392 (2001). \nhttps:\/\/doi.org\/10.1016\/S0304-3975(00)00102-X","journal-title":"Theoret. Comput. Sci."},{"key":"20_CR40","doi-asserted-by":"publisher","unstructured":"Fribourg, L., Ols\u00e9n, H.: Reachability sets of parameterized rings as regular languages. In: Moller, F. (ed.) Proceedings of 2nd International Workshop on Verification of Infinite State Systems, Infinity 1997, Bologna, Italy, 11\u201312 July 1997. Electronic Notes in Theoretical Computer Science, vol. 9, p. 40. Elsevier (1997). \nhttps:\/\/doi.org\/10.1016\/S1571-0661(05)80427-X","DOI":"10.1016\/S1571-0661(05)80427-X"},{"issue":"3","key":"20_CR41","doi-asserted-by":"publisher","first-page":"675","DOI":"10.1145\/146637.146681","volume":"39","author":"SM German","year":"1992","unstructured":"German, S.M., Sistla, A.P.: Reasoning about systems with many processes. J. ACM 39(3), 675\u2013735 (1992). \nhttps:\/\/doi.org\/10.1145\/146637.146681","journal-title":"J. ACM"},{"issue":"2","key":"20_CR42","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1016\/0020-0190(90)90107-9","volume":"35","author":"T Herman","year":"1990","unstructured":"Herman, T.: Probabilistic self-stabilization. Inf. Process. Lett. 35(2), 63\u201367 (1990). \nhttps:\/\/doi.org\/10.1016\/0020-0190(90)90107-9","journal-title":"Inf. Process. Lett."},{"key":"20_CR43","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1016\/0304-3975(79)90041-0","volume":"8","author":"JE Hopcroft","year":"1979","unstructured":"Hopcroft, J.E., Pansiot, J.: On the reachability problem for 5-dimensional vector addition systems. Theoret. Comput. Sci. 8, 135\u2013159 (1979). \nhttps:\/\/doi.org\/10.1016\/0304-3975(79)90041-0","journal-title":"Theoret. Comput. Sci."},{"key":"20_CR44","doi-asserted-by":"publisher","unstructured":"Israeli, A., Jalfon, M.: Token management schemes and random walks yield self-stabilizing mutual exclusion. In: Dwork, C. (ed.) Proceedings of 9th Annual ACM Symposium on Principles of Distributed Computing, PODC 1990, Quebec City, Quebec, Canada, 22\u201324 August 1990, pp. 119\u2013131. ACM (1990). \nhttps:\/\/doi.org\/10.1145\/93385.93409","DOI":"10.1145\/93385.93409"},{"issue":"6","key":"20_CR45","doi-asserted-by":"publisher","first-page":"537","DOI":"10.1007\/s00236-019-00338-6","volume":"56","author":"P Jancar","year":"2019","unstructured":"Jancar, P., Purser, D.: Structural liveness of petri nets is expspace-hard and decidable. Acta Inf. 56(6), 537\u2013552 (2019). \nhttps:\/\/doi.org\/10.1007\/s00236-019-00338-6","journal-title":"Acta Inf."},{"key":"20_CR46","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"645","DOI":"10.1007\/978-3-642-14295-6_55","volume-title":"Computer Aided Verification","author":"A Kaiser","year":"2010","unstructured":"Kaiser, A., Kroening, D., Wahl, T.: Dynamic cutoff detection in parameterized concurrent programs. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 645\u2013659. Springer, Heidelberg (2010). \nhttps:\/\/doi.org\/10.1007\/978-3-642-14295-6_55"},{"issue":"4","key":"20_CR47","doi-asserted-by":"publisher","first-page":"14:1","DOI":"10.1145\/2629608","volume":"36","author":"A Kaiser","year":"2014","unstructured":"Kaiser, A., Kroening, D., Wahl, T.: A widening approach to multithreaded program verification. ACM Trans. Program. Lang. Syst. 36(4), 14:1\u201314:29 (2014). \nhttps:\/\/doi.org\/10.1145\/2629608","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"20_CR48","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"543","DOI":"10.1007\/978-3-030-01090-4_34","volume-title":"Automated Technology for Verification and Analysis","author":"J K\u0159et\u00ednsk\u00fd","year":"2018","unstructured":"K\u0159et\u00ednsk\u00fd, J., Meggendorfer, T., Sickert, S.: Owl: a library for $$\\omega $$-words, automata, and LTL. In: Lahiri, S.K., Wang, C. (eds.) ATVA 2018. LNCS, vol. 11138, pp. 543\u2013550. Springer, Cham (2018). \nhttps:\/\/doi.org\/10.1007\/978-3-030-01090-4_34"},{"key":"20_CR49","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"585","DOI":"10.1007\/978-3-642-22110-1_47","volume-title":"Computer Aided Verification","author":"M Kwiatkowska","year":"2011","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 585\u2013591. Springer, Heidelberg (2011). \nhttps:\/\/doi.org\/10.1007\/978-3-642-22110-1_47"},{"key":"20_CR50","doi-asserted-by":"publisher","unstructured":"Lehmann, D., Rabin, M.O.: On the advantages of free choice: a symmetric and fully distributed solution to the dining philosophers problem. In: White, J., Lipton, R.J., Goldberg, P.C. (eds.) Proceedings of 8th Annual ACM Symposium on Principles of Programming Languages, POPL 1981, Williamsburg, Virginia, USA, January 1981, pp. 133\u2013138. ACM Press (1981). \nhttps:\/\/doi.org\/10.1145\/567532.567547","DOI":"10.1145\/567532.567547"},{"key":"20_CR51","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"499","DOI":"10.1007\/978-3-662-54577-5_29","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"O Leng\u00e1l","year":"2017","unstructured":"Leng\u00e1l, O., Lin, A.W., Majumdar, R., R\u00fcmmer, P.: Fair termination for parameterized probabilistic concurrent systems. In: Legay, A., Margaria, T. (eds.) TACAS 2017, Part I. LNCS, vol. 10205, pp. 499\u2013517. Springer, Heidelberg (2017). \nhttps:\/\/doi.org\/10.1007\/978-3-662-54577-5_29"},{"key":"20_CR52","doi-asserted-by":"publisher","unstructured":"Leroux, J.: Vector addition systems reachability problem (a simpler solution). In: Voronkov, A. (ed.) Proceedings of the Alan Turing Centenary Conference, Turing 100, Manchester, UK, 22\u201325 June 2012. EPiC Series in Computing, vol. 10, pp. 214\u2013228. EasyChair (2012). \nhttps:\/\/doi.org\/10.29007\/bnx2","DOI":"10.29007\/bnx2"},{"key":"20_CR53","doi-asserted-by":"publisher","unstructured":"Leroux, J.: Presburger vector addition systems. In: Proceedings of 28th Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS 2013, New Orleans, LA, USA, 25\u201328 June 2013. pp. 23\u201332. IEEE Computer Society (2013). \nhttps:\/\/doi.org\/10.1109\/LICS.2013.7","DOI":"10.1109\/LICS.2013.7"},{"key":"20_CR54","doi-asserted-by":"publisher","unstructured":"Leroux, J.: Vector addition system reversible reachability problem. Log. Methods Comput. Sci. 9(1) (2013). \nhttps:\/\/doi.org\/10.2168\/LMCS-9(1:5)2013","DOI":"10.2168\/LMCS-9(1:5)2013"},{"key":"20_CR55","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"112","DOI":"10.1007\/978-3-319-41540-6_7","volume-title":"Computer Aided Verification","author":"AW Lin","year":"2016","unstructured":"Lin, A.W., R\u00fcmmer, P.: Liveness of randomised parameterised systems under arbitrary schedulers. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016, Part II. LNCS, vol. 9780, pp. 112\u2013133. Springer, Cham (2016). \nhttps:\/\/doi.org\/10.1007\/978-3-319-41540-6_7"},{"issue":"1","key":"20_CR56","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. Cambridge Philos. Soc. 54(1), 60\u201371 (1958). \nhttps:\/\/doi.org\/10.1017\/S0305004100033193","journal-title":"Math. Proc. Cambridge Philos. Soc."},{"key":"20_CR57","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 de Moura","year":"2008","unstructured":"de 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). \nhttps:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"issue":"1","key":"20_CR58","doi-asserted-by":"publisher","first-page":"94","DOI":"10.1145\/2678280","volume":"58","author":"S Navlakha","year":"2015","unstructured":"Navlakha, S., Bar-Joseph, Z.: Distributed information processing in biological and computational systems. Commun. ACM 58(1), 94\u2013102 (2015). \nhttps:\/\/doi.org\/10.1145\/2678280","journal-title":"Commun. ACM"},{"key":"20_CR59","unstructured":"Nilsson, M.: Regular model checking. Ph.D. thesis, Uppsala University (2000)"},{"key":"20_CR60","doi-asserted-by":"publisher","unstructured":"Pang, J., Luo, Z., Deng, Y.: On automatic verification of self-stabilizing population protocols. In: Proceedings of 2nd IEEE\/IFIP International Symposium on Theoretical Aspects of Software Engineering, TASE 2008, 17\u201319 June 2008, Nanjing, China, pp. 185\u2013192. IEEE Computer Society (2008). \nhttps:\/\/doi.org\/10.1109\/TASE.2008.8","DOI":"10.1109\/TASE.2008.8"},{"issue":"3","key":"20_CR61","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1016\/0020-0190(81)90106-X","volume":"12","author":"GL Peterson","year":"1981","unstructured":"Peterson, G.L.: Myths about the mutual exclusion problem. Inf. Process. Lett. 12(3), 115\u2013116 (1981). \nhttps:\/\/doi.org\/10.1016\/0020-0190(81)90106-X","journal-title":"Inf. Process. Lett."},{"key":"20_CR62","unstructured":"Presburger, M.: \u00dcber die Vollst\u00e4ndigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt. Comptes Rendus du $$\\text{I}^\\text{ er }$$ Congr\u00e8s des math\u00e9maticiens des pays slaves, pp. 192\u2013201 (1929)"},{"key":"20_CR63","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). \nhttps:\/\/doi.org\/10.1007\/978-3-642-02658-4_59"},{"key":"20_CR64","doi-asserted-by":"publisher","unstructured":"Szymanski, B.K.: A simple solution to Lamport\u2019s concurrent programming problem with linear wait. In: Lenfant, J. (ed.) Proceedings of 2nd International Conference on Supercomputing, ICS 1988, Saint Malo, France, 4\u20138 July 1988, pp. 621\u2013626. ACM (1988). \nhttps:\/\/doi.org\/10.1145\/55364.55425","DOI":"10.1145\/55364.55425"},{"key":"20_CR65","doi-asserted-by":"publisher","unstructured":"Vardi, M.Y.: Automatic verification of probabilistic concurrent finite-state programs. In: Proceedings of 26th Annual Symposium on Foundations of Computer Science, FOCS 1985, Portland, Oregon, USA, 21\u201323 October 1985, pp. 327\u2013338. IEEE Computer Society (1985). \nhttps:\/\/doi.org\/10.1109\/SFCS.1985.12","DOI":"10.1109\/SFCS.1985.12"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-53291-8_20","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,7,15]],"date-time":"2020-07-15T20:07:47Z","timestamp":1594843667000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-53291-8_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030532901","9783030532918"],"references-count":65,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-53291-8_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020]]},"assertion":[{"value":"14 July 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Los Angeles, CA","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"USA","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2020","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"21 July 2020","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24 July 2020","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"32","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2020","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/i-cav.org\/2020\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair.org","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"240","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"43","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"22","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"18% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"4","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"11","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"The conference was held virtually due to the COVID-19 pandemic.","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}