{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T07:24:40Z","timestamp":1740122680384,"version":"3.37.3"},"reference-count":40,"publisher":"Springer Science and Business Media LLC","issue":"1-3","license":[{"start":{"date-parts":[[2023,7,7]],"date-time":"2023-07-07T00:00:00Z","timestamp":1688688000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2023,7,7]],"date-time":"2023-07-07T00:00:00Z","timestamp":1688688000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100005760","name":"University of Gothenburg","doi-asserted-by":"crossref","id":[{"id":"10.13039\/501100005760","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2024,6]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We consider systems with unboundedly many processes that communicate through shared memory. In that context, simple verification questions have a high complexity or, in the case of pushdown processes, are even undecidable. Good algorithmic properties are recovered under round-bounded verification, which restricts the system behavior to a bounded number of round-robin schedules. In this paper, we extend this approach to a game-based setting. This allows one to solve synthesis and control problems and constitutes a further step towards a theory of languages over infinite alphabets.<\/jats:p>","DOI":"10.1007\/s10703-023-00431-0","type":"journal-article","created":{"date-parts":[[2023,7,7]],"date-time":"2023-07-07T03:36:08Z","timestamp":1688700968000},"page":"41-78","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Round- and context-bounded control of dynamic pushdown systems"],"prefix":"10.1007","volume":"62","author":[{"given":"Benedikt","family":"Bollig","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6205-0682","authenticated-orcid":false,"given":"Mathieu","family":"Lehaut","sequence":"additional","affiliation":[]},{"given":"Nathalie","family":"Sznajder","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2023,7,7]]},"reference":[{"key":"431_CR1","doi-asserted-by":"crossref","unstructured":"Abdulla PA, Bouajjani A, d\u2019Orso J (2003) Deciding monotonic games. In: CSL\u201903, volume 2803 of LNCS, pages 1\u201314. Springer","DOI":"10.1007\/978-3-540-45220-1_1"},{"issue":"5","key":"431_CR2","doi-asserted-by":"publisher","first-page":"469","DOI":"10.1007\/s10009-016-0424-3","volume":"18","author":"PA Abdulla","year":"2016","unstructured":"Abdulla PA, Delzanno G (2016) Parameterized verification. Int. J. Softw. Tools Technol. Transf. 18(5):469\u2013473","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"431_CR3","doi-asserted-by":"crossref","unstructured":"Abdulla PA, Mayr R, Sangnier A, Sproston J (2013) Solving parity games on integer vectors. In: CONCUR\u201913, volume 8052, pages 106\u2013120. Springer","DOI":"10.1007\/978-3-642-40184-8_9"},{"key":"431_CR4","doi-asserted-by":"crossref","unstructured":"Aminof B, Jacobs S, Khalimov A, Rubin S (2014) Parameterized model checking of token-passing systems. In: VMCAI\u201914, volume 8318 of LNCS, pp. 262\u2013281. Springer","DOI":"10.1007\/978-3-642-54013-4_15"},{"key":"431_CR5","doi-asserted-by":"crossref","unstructured":"Atig MF, Bouajjani A, Narayan Kumar K, Saivasan P (2017) Parity games on bounded phase multi-pushdown systems. In: NETYS\u201917, volume 10299 of LNCS, pp. 272\u2013287","DOI":"10.1007\/978-3-319-59647-1_21"},{"issue":"4","key":"431_CR6","first-page":"7","volume":"7","author":"MF Atig","year":"2011","unstructured":"Atig MF, Bouajjani A, Qadeer S (2011) Context-bounded analysis for concurrent programs with dynamic creation of threads. Log. Methods Comput. Sci. 7(4):7","journal-title":"Log. Methods Comput. Sci."},{"key":"431_CR7","doi-asserted-by":"crossref","unstructured":"B\u00e9rard B, Haddad S, Sassolas M, Sznajder N (2012) Concurrent games on VASS with inhibition. In: CONCUR\u201912, volume 7454 of LNCS, pp. 39\u201352. Springer","DOI":"10.1007\/978-3-642-32940-1_5"},{"issue":"4\u20135","key":"431_CR8","doi-asserted-by":"publisher","first-page":"702","DOI":"10.1016\/j.tcs.2009.10.009","volume":"411","author":"H Bj\u00f6rklund","year":"2010","unstructured":"Bj\u00f6rklund H, Schwentick T (2010) On notions of regularity for data languages. Theoret Comput Sci 411(4\u20135):702\u2013715","journal-title":"Theoret Comput Sci"},{"issue":"4","key":"431_CR9","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1145\/1970398.1970403","volume":"12","author":"M Boja\u0144czyk","year":"2011","unstructured":"Boja\u0144czyk M, David C, Muscholl A, Schwentick T, Segoufin L (2011) Two-variable logic on data words. ACM Trans Comput Log 12(4):27","journal-title":"ACM Trans Comput Log"},{"key":"431_CR10","doi-asserted-by":"crossref","unstructured":"Bollig Benedikt, Lehaut Mathieu, Sznajder Nathalie (2018) Round-bounded control of parameterized systems. In: 16th international symposium on automated technology for verification and analysis, Proceedings of ATVA\u201918, volume 11138 of Lecture notes in computer science, pages 370\u2013386. Springer","DOI":"10.1007\/978-3-030-01090-4_22"},{"key":"431_CR11","doi-asserted-by":"crossref","unstructured":"Bollig Benedikt, Lehaut Mathieu, Sznajder Nathalie (2019) Round-bounded control of parameterized systems. Technical Report hal-01849206, HAL, March","DOI":"10.1007\/978-3-030-01090-4_22"},{"key":"431_CR12","doi-asserted-by":"crossref","unstructured":"Bouajjani Ahmed, Esparza Javier, Schwoon Stefan, Strejcek Jan (2005) Reachability analysis of multithreaded software with asynchronous communication. In: FSTTCS 2005: Foundations of software technology and theoretical computer science, 25th international conference, Hyderabad, India, December 15-18, 2005, Proceedings, volume 3821 of Lecture notes in computer science, pages 348\u2013359. Springer","DOI":"10.1007\/11590156_28"},{"key":"431_CR13","doi-asserted-by":"crossref","unstructured":"Br\u00e1zdil T, Jancar P, Kucera A (2010) Reachability games on extended vector addition systems with states. In: ICALP\u201910, Part II, volume 6199 of LNCS, pp. 478\u2013489. Springer","DOI":"10.1007\/978-3-642-14162-1_40"},{"key":"431_CR14","doi-asserted-by":"crossref","unstructured":"Br\u00fctsch B, Thomas W (2016) Playing games in the Baire space. In: Proc. Cassting Workshop on Games for the Synthesis of Complex Systems and 3rd Int. workshop on synthesis of complex parameters volume 220 of EPTCS, pages 13\u201325","DOI":"10.4204\/EPTCS.220.2"},{"key":"431_CR15","doi-asserted-by":"crossref","unstructured":"Courtois J-B, Schmitz S (2014) Alternating vector addition systems with states. In: MFCS\u201914, volume 8634 of LNCS, pages 220\u2013231. Springer","DOI":"10.1007\/978-3-662-44522-8_19"},{"issue":"1","key":"431_CR16","first-page":"7:1","volume":"68","author":"Czerwinski Wojciech","year":"2021","unstructured":"Wojciech Czerwinski, Slawomir Lasota, Ranko Lazic, J\u00e9r\u00f4me Leroux, Filip Mazowiecki (2021) The reachability problem for petri nets is not elementary. J ACM 68(1):7:1-7:28","journal-title":"J ACM"},{"key":"431_CR17","doi-asserted-by":"crossref","unstructured":"Ehlers R\u00fcdiger, Seshia Sanjit\u00a0A, Kress-Gazit Hadas (2014) Synthesis with identifiers. In: international conference on verification, model checking, and abstract interpretation, pages 415\u2013433. Springer","DOI":"10.1007\/978-3-642-54013-4_23"},{"key":"431_CR18","doi-asserted-by":"crossref","unstructured":"Emerson EA, Jutla CS (1991) Tree automata, mu-calculus and determinacy. In: proceedings of FOCS\u201991, pages 368\u2013377. IEEE computer society","DOI":"10.1109\/SFCS.1991.185392"},{"issue":"4","key":"431_CR19","doi-asserted-by":"publisher","first-page":"527","DOI":"10.1142\/S0129054103001881","volume":"14","author":"EA Emerson","year":"2003","unstructured":"Emerson EA, Namjoshi KS (2003) On reasoning about rings. Int. J. Found. Comput. S. 14(4):527\u2013550","journal-title":"Int. J. Found. Comput. S."},{"key":"431_CR20","unstructured":"Esparza J (2014) Keeping a crowd safe: On the complexity of parameterized verification. In: STACS\u201914, volume\u00a025 of Leibniz international proceedings in informatics, pages 1\u201310. Leibniz-Zentrum f\u00fcr Informatik"},{"key":"431_CR21","unstructured":"Exibard L\u00e9o, Filiot Emmanuel, Reynier Pierre-Alain (2019) Synthesis of data word transducers. In: 30th international conference on concurrency theory"},{"key":"431_CR22","doi-asserted-by":"crossref","unstructured":"Figueira D., Praveen M (2018) Playing with repetitions in data words using energy games. In: proceedings of LICS\u201918, pages 404\u2013413. ACM","DOI":"10.1145\/3209108.3209154"},{"issue":"1","key":"431_CR23","first-page":"151","volume":"10","author":"S Jacobs","year":"2014","unstructured":"Jacobs S, Bloem R (2014) Parameterized synthesis. Log Methods Comput Sci 10(1):151","journal-title":"Log Methods Comput Sci"},{"key":"431_CR24","doi-asserted-by":"crossref","unstructured":"Jancar P (2015) On reachability-related games on vector addition systems with states. In: RP\u201915, volume 9328 of LNCS, pages 50\u201362. Springer","DOI":"10.1007\/978-3-319-24537-9_6"},{"key":"431_CR25","unstructured":"Kara A (2016) Logics on data words: Expressivity, satisfiability, model checking. PhD thesis, Technical University of Dortmund"},{"key":"431_CR26","doi-asserted-by":"crossref","unstructured":"Khalimov Ayrat, Maderbacher Benedikt, Bloem Roderick (2018) Bounded synthesis of register transducers. In: international symposium on automated technology for verification and analysis, pages 494\u2013510. Springer","DOI":"10.1007\/978-3-030-01090-4_29"},{"key":"431_CR27","doi-asserted-by":"crossref","unstructured":"La Torre S, Madhusudan P, Parlato G (2007) A robust class of context-sensitive languages. In: LICS\u201907, pages 161\u2013170. IEEE Computer Society Press","DOI":"10.1109\/LICS.2007.9"},{"key":"431_CR28","doi-asserted-by":"crossref","unstructured":"Torre SLa, Madhusudan P., Parlato G (2008) Context-bounded analysis of concurrent queue systems. In: proceedings of TACAS\u201908, volume 4963 of LNCS, pp. 299\u2013314. Springer","DOI":"10.1007\/978-3-540-78800-3_21"},{"key":"431_CR29","doi-asserted-by":"crossref","unstructured":"Torre SLa, Madhusudan P, Parlato G (2010) Model-checking parameterized concurrent programs using linear interfaces. In: CAV\u201910, volume 6174 of LNCS, pp. 629\u2013644. Springer","DOI":"10.1007\/978-3-642-14295-6_54"},{"key":"431_CR30","unstructured":"Torre SLa, Madhusudan P, Parlato G (2010) Model-checking parameterized concurrent programs using linear interfaces. Technical report 2142\/15410, University of Illinois, Available at http:\/\/hdl.handle.net\/2142\/15410"},{"issue":"4","key":"431_CR31","doi-asserted-by":"publisher","first-page":"623","DOI":"10.1093\/logcom\/12.4.623","volume":"12","author":"M Lange","year":"2002","unstructured":"Lange M, Stirling C (2002) Model checking games for branching time logics. J Log Comput 12(4):623\u2013639","journal-title":"J Log Comput"},{"issue":"3","key":"431_CR32","doi-asserted-by":"publisher","first-page":"441","DOI":"10.1137\/0213029","volume":"13","author":"Ernst W Mayr","year":"1984","unstructured":"Mayr Ernst W (1984) An algorithm for the general petri net reachability problem. SIAM J Comput 13(3):441\u2013460","journal-title":"SIAM J Comput"},{"key":"431_CR33","volume-title":"Computation: finite and infinite machines","author":"Marvin L Minsky","year":"1967","unstructured":"Minsky Marvin L (1967) Computation: finite and infinite machines. Prentice Hall, Upper Saddle River, NJ, USA"},{"key":"431_CR34","doi-asserted-by":"crossref","unstructured":"Qadeer S, Rehof J (2005) Context-bounded model checking of concurrent software. In: TACAS\u201905, volume 3440 of LNCS, pages 93\u2013107. Springer","DOI":"10.1007\/978-3-540-31980-1_7"},{"issue":"2","key":"431_CR35","doi-asserted-by":"publisher","first-page":"416","DOI":"10.1145\/349214.349241","volume":"22","author":"G Ramalingam","year":"2000","unstructured":"Ramalingam G (2000) Context-sensitive synchronization-sensitive analysis is undecidable. ACM Trans Program Lang Syst 22(2):416\u2013430","journal-title":"ACM Trans Program Lang Syst"},{"key":"431_CR36","doi-asserted-by":"crossref","unstructured":"Seth A (2009) Games on multi-stack pushdown systems. In: LFCS\u201909, volume 5407 of LNCS, pages 395\u2013408. Springer","DOI":"10.1007\/978-3-540-92687-0_27"},{"key":"431_CR37","unstructured":"Stockmeyer LJ (1974) The complexity of decision problems in automata theory and logic. PhD thesis, MIT"},{"key":"431_CR38","doi-asserted-by":"crossref","unstructured":"Thomas W (1997) Languages, automata and logic. In: Salomaa A, Rozenberg G. editors, Handbook of formal languages, volume\u00a03, pages 389\u2013455. Springer","DOI":"10.1007\/978-3-642-59126-6_7"},{"issue":"2","key":"431_CR39","doi-asserted-by":"publisher","first-page":"234","DOI":"10.1006\/inco.2000.2894","volume":"164","author":"I Walukiewicz","year":"2001","unstructured":"Walukiewicz I (2001) Pushdown processes: games and model-checking. Inf Comput 164(2):234\u2013263","journal-title":"Inf Comput"},{"issue":"1\u20132","key":"431_CR40","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1016\/S0304-3975(98)00009-7","volume":"200","author":"W Zielonka","year":"1998","unstructured":"Zielonka W (1998) Infinite games on finitely coloured graphs with applications to automata on infinite trees. TCS 200(1\u20132):135\u2013183","journal-title":"TCS"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-023-00431-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10703-023-00431-0\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-023-00431-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,10,23]],"date-time":"2024-10-23T19:45:16Z","timestamp":1729712716000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10703-023-00431-0"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,7,7]]},"references-count":40,"journal-issue":{"issue":"1-3","published-print":{"date-parts":[[2024,6]]}},"alternative-id":["431"],"URL":"https:\/\/doi.org\/10.1007\/s10703-023-00431-0","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"type":"print","value":"0925-9856"},{"type":"electronic","value":"1572-8102"}],"subject":[],"published":{"date-parts":[[2023,7,7]]},"assertion":[{"value":"12 October 2022","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"5 June 2023","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"7 July 2023","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}