{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,7]],"date-time":"2026-10-07T20:16:47Z","timestamp":1791404207839,"version":"4.3.3"},"reference-count":31,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2016,2,19]],"date-time":"2016-02-19T00:00:00Z","timestamp":1455840000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["J. ACM"],"published-print":{"date-parts":[[2016,3,30]]},"abstract":"<jats:p>We characterize the complexity of the safety verification problem for parameterized systems consisting of a leader process and arbitrarily many anonymous and identical contributors. Processes communicate through a shared, bounded-value register. While each operation on the register is atomic, there is no synchronization primitive to execute a sequence of operations atomically.<\/jats:p>\n          <jats:p>We analyze the complexity of the safety verification problem when processes are modeled by finite-state machines, pushdown machines, and Turing machines. The problem is coNP-complete when all processes are finite-state machines, and is PSPACE-complete when they are pushdown machines. The complexity remains coNP-complete when each Turing machine is allowed boundedly many interactions with the register. Our proofs use combinatorial characterizations of computations in the model, and in the case of pushdown systems, some language-theoretic constructions of independent interest. Our results are surprising, because parameterized verification problems on slight variations of our model are known to be undecidable. For example, the problem is undecidable for finite-state machines operating with synchronization primitives, and already for two communicating pushdown machines. Thus, our results show that a robust, decidable class can be obtained under the assumptions of anonymity and asynchrony.<\/jats:p>","DOI":"10.1145\/2842603","type":"journal-article","created":{"date-parts":[[2016,2,22]],"date-time":"2016-02-22T13:07:16Z","timestamp":1456146436000},"page":"1-48","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":20,"title":["Parameterized Verification of Asynchronous Shared-Memory Systems"],"prefix":"10.1145","volume":"63","author":[{"given":"Javier","family":"Esparza","sequence":"first","affiliation":[{"name":"Fakult\u00e4t f\u00fcr Informatik, Technische Universit\u00e4t M\u00fcnchen, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Pierre","family":"Ganty","sequence":"additional","affiliation":[{"name":"IMDEA Software Institute, Madrid, Spain"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Rupak","family":"Majumdar","sequence":"additional","affiliation":[{"name":"Max Planck Institute for Software Systems, Kaiserslautern, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2016,2,19]]},"reference":[{"key":"e_1_2_1_1_1","volume-title":"LICS\u201996","author":"Abdulla Parosh Aziz","unstructured":"Parosh Aziz Abdulla , Karlis Cerans , Bengt Jonsson , and Yih-Kuen Tsay . 1996. General decidability theorems for infinite-state systems . In LICS\u201996 . IEEE Computer Society , 313--321. DOI:http:\/\/dx.doi.org\/ 10.1109\/LICS.1996.561359 10.1109\/LICS.1996.561359 Parosh Aziz Abdulla, Karlis Cerans, Bengt Jonsson, and Yih-Kuen Tsay. 1996. General decidability theorems for infinite-state systems. In LICS\u201996. IEEE Computer Society, 313--321. DOI:http:\/\/dx.doi.org\/ 10.1109\/LICS.1996.561359"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00446-007-0040-2"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(86)90071-2"},{"key":"e_1_2_1_4_1","volume-title":"Computational Complexity--A Modern Approach","author":"Arora Sanjeev","unstructured":"Sanjeev Arora and Boaz Barak . 2009. Computational Complexity--A Modern Approach . Cambridge University Press , New York, NY . Sanjeev Arora and Boaz Barak. 2009. Computational Complexity--A Modern Approach. Cambridge University Press, New York, NY."},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0019-9958(67)90771-1"},{"key":"e_1_2_1_6_1","series-title":"Lecture Notes in Computer Science","volume-title":"TACAS\u201908","author":"Clarke Edmund M.","unstructured":"Edmund M. Clarke , Muralidhar Talupur , and Helmut Veith . 2008. Proving ptolemy right: The environment abstraction framework for model checking concurrent systems . In TACAS\u201908 . Lecture Notes in Computer Science , Vol. 4963 . Springer , Berlin , 33--47. DOI:http:\/\/dx.doi.org\/10.1007\/978-3-540-78800-3_4 10.1007\/978-3-540-78800-3_4 Edmund M. Clarke, Muralidhar Talupur, and Helmut Veith. 2008. Proving ptolemy right: The environment abstraction framework for model checking concurrent systems. In TACAS\u201908. Lecture Notes in Computer Science, Vol. 4963. Springer, Berlin, 33--47. DOI:http:\/\/dx.doi.org\/10.1007\/978-3-540-78800-3_4"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1026276129010"},{"key":"e_1_2_1_8_1","series-title":"Lecture Notes in Computer Science","volume-title":"TACAS\u201902","author":"Delzanno Giorgio","unstructured":"Giorgio Delzanno , Jean-Fran\u00e7ois Raskin , and Laurent Van Begin . 2002. Towards the automated verification of multithreaded Java programs . In TACAS\u201902 . Lecture Notes in Computer Science , Vol. 2280 . Springer , Berline , 173--187. DOI:http:\/\/dx.doi.org\/10.1007\/3-540-46002-0_13 10.1007\/3-540-46002-0_13 Giorgio Delzanno, Jean-Fran\u00e7ois Raskin, and Laurent Van Begin. 2002. Towards the automated verification of multithreaded Java programs. In TACAS\u201902. Lecture Notes in Computer Science, Vol. 2280. Springer, Berline, 173--187. DOI:http:\/\/dx.doi.org\/10.1007\/3-540-46002-0_13"},{"key":"e_1_2_1_9_1","series-title":"Lecture Notes in Computer Science","volume-title":"CONCUR\u201910","author":"Delzanno Giorgio","unstructured":"Giorgio Delzanno , Arnaud Sangnier , and Gianluigi Zavattaro . 2010. Parameterized verification of ad hoc networks . In CONCUR\u201910 . Lecture Notes in Computer Science , Vol. 6269 . Springer , Berline , 313--327. DOI:http:\/\/dx.doi.org\/10.1007\/978-3-642-15375-4_22 10.1007\/978-3-642-15375-4_22 Giorgio Delzanno, Arnaud Sangnier, and Gianluigi Zavattaro. 2010. Parameterized verification of ad hoc networks. In CONCUR\u201910. Lecture Notes in Computer Science, Vol. 6269. Springer, Berline, 313--327. DOI:http:\/\/dx.doi.org\/10.1007\/978-3-642-15375-4_22"},{"key":"e_1_2_1_10_1","series-title":"Lecture Notes in Computer Science","volume-title":"Is lazy abstraction a decision procedure for broadcast protocols? In VMCAI\u201908","author":"Dimitrova Rayna","unstructured":"Rayna Dimitrova and Andreas Podelski . 2008. Is lazy abstraction a decision procedure for broadcast protocols? In VMCAI\u201908 . Lecture Notes in Computer Science , Vol. 4905 . Springer , Berlin , 98--111. DOI:http:\/\/dx.doi.org\/10.1007\/978-3-540-78163-9_12 10.1007\/978-3-540-78163-9_12 Rayna Dimitrova and Andreas Podelski. 2008. Is lazy abstraction a decision procedure for broadcast protocols? In VMCAI\u201908. Lecture Notes in Computer Science, Vol. 4905. Springer, Berlin, 98--111. DOI:http:\/\/dx.doi.org\/10.1007\/978-3-540-78163-9_12"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/10722167"},{"key":"e_1_2_1_12_1","volume-title":"Namjoshi","author":"Allen Emerson E.","year":"1998","unstructured":"E. Allen Emerson and Kedar S . Namjoshi . 1998 . Verification of parameterized bus arbitration protocol. In CAV\u201998. Lecture Notes in Computer Science, Vol. 1427 . Springer , Berlin, 452--463. DOI:http:\/\/dx.doi.org\/ 10.1007\/BFb0028766 10.1007\/BFb0028766 E. Allen Emerson and Kedar S. Namjoshi. 1998. Verification of parameterized bus arbitration protocol. In CAV\u201998. Lecture Notes in Computer Science, Vol. 1427. Springer, Berlin, 452--463. DOI:http:\/\/dx.doi.org\/ 10.1007\/BFb0028766"},{"key":"e_1_2_1_13_1","volume-title":"STACS\u201914: 31st International Symposium on Theoretical Aspects of Computer Science (Leibniz International Proceedings in Informatics (LIPIcs)","volume":"25","author":"Esparza Javier","year":"2014","unstructured":"Javier Esparza . 2014 . Keeping a crowd safe: On the complexity of parameterized verification (invited talk) . In STACS\u201914: 31st International Symposium on Theoretical Aspects of Computer Science (Leibniz International Proceedings in Informatics (LIPIcs) , Vol. 25 . Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, 1--10. DOI:http:\/\/dx.doi.org\/10.4230\/LIPIcs.STACS. 2014.1 10.4230\/LIPIcs.STACS.2014.1 Javier Esparza. 2014. Keeping a crowd safe: On the complexity of parameterized verification (invited talk). In STACS\u201914: 31st International Symposium on Theoretical Aspects of Computer Science (Leibniz International Proceedings in Informatics (LIPIcs), Vol. 25. Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, 1--10. DOI:http:\/\/dx.doi.org\/10.4230\/LIPIcs.STACS.2014.1"},{"key":"e_1_2_1_14_1","volume-title":"LICS\u201999","author":"Esparza Javier","unstructured":"Javier Esparza , Alain Finkel , and Richard Mayr . 1999. On the verification of broadcast protocols . In LICS\u201999 . IEEE Computer Society , 352--359. DOI:http:\/\/dx.doi.org\/10.1109\/LICS.1999.782630 10.1109\/LICS.1999.782630 Javier Esparza, Alain Finkel, and Richard Mayr. 1999. On the verification of broadcast protocols. In LICS\u201999. IEEE Computer Society, 352--359. DOI:http:\/\/dx.doi.org\/10.1109\/LICS.1999.782630"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ipl.2011.03.019"},{"key":"e_1_2_1_16_1","series-title":"Lecture Notes in Computer Science","volume-title":"FSTTCS\u201902","author":"Finkel Alain","unstructured":"Alain Finkel and J\u00e9r\u00f4me Leroux . 2002. How to compose Presburger-accelerations: Applications to broadcast protocols . In FSTTCS\u201902 . Lecture Notes in Computer Science , Vol. 2556 . Springer , Berlin , 145--156. DOI:http:\/\/dx.doi.org\/10.1007\/3-540-36206-1_14 10.1007\/3-540-36206-1_14 Alain Finkel and J\u00e9r\u00f4me Leroux. 2002. How to compose Presburger-accelerations: Applications to broadcast protocols. In FSTTCS\u201902. Lecture Notes in Computer Science, Vol. 2556. Springer, Berlin, 145--156. DOI:http:\/\/dx.doi.org\/10.1007\/3-540-36206-1_14"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/2160910.2160915"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/146637.146681"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00446-007-0042-0"},{"key":"e_1_2_1_20_1","volume-title":"Proceedings of FSTTCS\u201911 (LIPIcs)","volume":"13","author":"Hague Matthew","year":"2011","unstructured":"Matthew Hague . 2011 . Parameterised pushdown systems with non-atomic writes . In Proceedings of FSTTCS\u201911 (LIPIcs) , Vol. 13 . Schloss Dagstuhl, 457--468. DOI:http:\/\/dx.doi.org\/10.4230\/LIPIcs.FSTTCS. 2011.457 10.4230\/LIPIcs.FSTTCS Matthew Hague. 2011. Parameterised pushdown systems with non-atomic writes. In Proceedings of FSTTCS\u201911 (LIPIcs), Vol. 13. Schloss Dagstuhl, 457--468. DOI:http:\/\/dx.doi.org\/10.4230\/LIPIcs.FSTTCS. 2011.457"},{"key":"e_1_2_1_21_1","volume-title":"Ullman","author":"Hopcroft John E.","year":"1979","unstructured":"John E. Hopcroft and Jeffrey D . Ullman . 1979 . Introduction to Automata Theory, Languages and Computation (1st ed.). Addison-Wesley , New York, NY. John E. Hopcroft and Jeffrey D. Ullman. 1979. Introduction to Automata Theory, Languages and Computation (1st ed.). Addison-Wesley, New York, NY."},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/800119.803883"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14295-6_55"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1109\/LCN.2007.143"},{"key":"e_1_2_1_25_1","series-title":"Lecture Notes in Computer Science","volume-title":"CAV\u201998","author":"McMillan Kenneth L.","unstructured":"Kenneth L. McMillan . 1998. Verification of an implementation of Tomasulo\u2019s algorithm by compositional model checking . In CAV\u201998 . Lecture Notes in Computer Science , Vol. 1427 . Springer , Berlin , 110--121. DOI:http:\/\/dx.doi.org\/10.1007\/BFb0028738 10.1007\/BFb0028738 Kenneth L. McMillan. 1998. Verification of an implementation of Tomasulo\u2019s algorithm by compositional model checking. In CAV\u201998. Lecture Notes in Computer Science, Vol. 1427. Springer, Berlin, 110--121. DOI:http:\/\/dx.doi.org\/10.1007\/BFb0028738"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1126\/science.1254295"},{"key":"e_1_2_1_27_1","volume-title":"Introduction to the Theory of Computation","author":"Sipser M.","unstructured":"M. Sipser . 1996. Introduction to the Theory of Computation . International Thomson Publishing . M. Sipser. 1996. Introduction to the Theory of Computation. International Thomson Publishing."},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14295-6_54"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2009.01.021"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1126\/science.1245842"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1038\/scientificamerican0313-60"}],"container-title":["Journal of the ACM"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2842603","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2842603","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:53:48Z","timestamp":1750222428000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2842603"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,2,19]]},"references-count":31,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2016,3,30]]}},"alternative-id":["10.1145\/2842603"],"URL":"https:\/\/doi.org\/10.1145\/2842603","relation":{},"ISSN":["0004-5411","1557-735X"],"issn-type":[{"value":"0004-5411","type":"print"},{"value":"1557-735X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016,2,19]]},"assertion":[{"value":"2014-11-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2015-10-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2016-02-19","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}