{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,13]],"date-time":"2025-05-13T16:17:50Z","timestamp":1747153070865,"version":"3.40.5"},"publisher-location":"Cham","reference-count":38,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030897154"},{"type":"electronic","value":"9783030897161"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2021,10,22]],"date-time":"2021-10-22T00:00:00Z","timestamp":1634860800000},"content-version":"vor","delay-in-days":294,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Valence systems are an abstract model of computation that consists of a finite-state control and some storage mechanism. In contrast to traditional models, the storage mechanism is not fixed, but given as a parameter. This allows us to precisely state questions like: For which storage mechanisms is the reachability problem decidable?<\/jats:p><jats:p>This survey reports on recent results that aim to understand the impact of the storage mechanism on decidability and complexity of several variants of the reachability problem. The considered problems are configuration reachability, model-checking first-order logic with reachability, and reachability under bounded context switching and scope-boundedness.<\/jats:p>","DOI":"10.1007\/978-3-030-89716-1_4","type":"book-chapter","created":{"date-parts":[[2021,10,25]],"date-time":"2021-10-25T09:08:02Z","timestamp":1635152882000},"page":"52-65","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Recent Advances on Reachability Problems for Valence Systems (Invited Talk)"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-6421-4388","authenticated-orcid":false,"given":"Georg","family":"Zetzsche","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2021,10,22]]},"reference":[{"key":"4_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1007\/978-3-642-40313-2_22","volume-title":"Mathematical Foundations of Computer Science 2013","author":"P Buckheister","year":"2013","unstructured":"Buckheister, P., Zetzsche, G.: Semilinearity and context-freeness of languages accepted by valence automata. In: Chatterjee, K., Sgall, J. (eds.) MFCS 2013. LNCS, vol. 8087, pp. 231\u2013242. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-40313-2_22"},{"key":"4_CR2","doi-asserted-by":"publisher","unstructured":"Chomsky, N., Sch\u00fctzenberger, M.P.: The algebraic theory of context-free languages. In: Computer Programming and Formal Systems, pp. 118\u2013161. North-Holland, Amsterdam (1963). https:\/\/doi.org\/10.1016\/S0049-237X(08)72023-8","DOI":"10.1016\/S0049-237X(08)72023-8"},{"key":"4_CR3","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: Proceedings of the 51st Annual ACM SIGACT Symposium on Theory of Computing (STOC 2019), pp. 24\u201333. ACM (2019). https:\/\/doi.org\/10.1145\/3313276.3316369","DOI":"10.1145\/3313276.3316369"},{"key":"4_CR4","unstructured":"Czerwinski, W., Orlikowski, L.: Reachability in vector addition systems is Ackermann-complete. CoRR abs\/2104.13866 (2021). https:\/\/arxiv.org\/abs\/2104.13866"},{"key":"4_CR5","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-74932-2","volume-title":"Regulated Rewriting in Formal Language Theory","author":"J Dassow","year":"1989","unstructured":"Dassow, J., P\u0103un, G.: Regulated Rewriting in Formal Language Theory. Springer, Heidelberg (1989)"},{"key":"4_CR6","doi-asserted-by":"publisher","unstructured":"D\u2019Osualdo, E., Meyer, R., Zetzsche, G.: First-order logic with reachability for infinite-state systems. In: Proceedings of the 31st Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS 2016), pp. 457\u2013466. ACM (2016). https:\/\/doi.org\/10.1145\/2933575.2934552","DOI":"10.1145\/2933575.2934552"},{"key":"4_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1007\/BFb0055044","volume-title":"Automata, Languages and Programming","author":"C Dufourd","year":"1998","unstructured":"Dufourd, C., Finkel, A., Schnoebelen, P.: Reset nets between decidability and undecidability. In: Larsen, K.G., Skyum, S., Winskel, G. (eds.) ICALP 1998. LNCS, vol. 1443, pp. 103\u2013115. Springer, Heidelberg (1998). https:\/\/doi.org\/10.1007\/BFb0055044"},{"key":"4_CR8","doi-asserted-by":"publisher","first-page":"106079","DOI":"10.1016\/j.ipl.2020.106079","volume":"167","author":"M Englert","year":"2021","unstructured":"Englert, M., et al.: A lower bound for the coverability problem in acyclic pushdown VAS. Inf. Process. Lett. 167, 106079 (2021). https:\/\/doi.org\/10.1016\/j.ipl.2020.106079","journal-title":"Inf. Process. Lett."},{"key":"4_CR9","doi-asserted-by":"crossref","unstructured":"Esparza, J., Ganty, P., Poch, T.: Pattern-based verification for multithreaded programs. ACM ToPLaS 36(3), 9:1\u20139:29 (2014)","DOI":"10.1145\/2629644"},{"key":"4_CR10","doi-asserted-by":"publisher","first-page":"377","DOI":"10.1016\/S0304-3975(01)00282-1","volume":"276","author":"H Fernau","year":"2002","unstructured":"Fernau, H., Stiebe, R.: Sequential grammars and automata with valences. Theoret. Comput. Sci. 276, 377\u2013405 (2002). https:\/\/doi.org\/10.1016\/S0304-3975(01)00282-1","journal-title":"Theoret. Comput. Sci."},{"key":"4_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"346","DOI":"10.1007\/3-540-46541-3_29","volume-title":"STACS 2000","author":"A Finkel","year":"2000","unstructured":"Finkel, A., Sutre, G.: Decidability of reachability problems for classes of two counters automata. In: Reichel, H., Tison, S. (eds.) STACS 2000. LNCS, vol. 1770, pp. 346\u2013357. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/3-540-46541-3_29"},{"key":"4_CR12","doi-asserted-by":"publisher","first-page":"311","DOI":"10.1016\/0304-3975(78)90020-8","volume":"7","author":"SA Greibach","year":"1978","unstructured":"Greibach, S.A.: Remarks on blind and partially blind one-way multicounter machines. Theor. Comput. Sci. 7, 311\u2013324 (1978). https:\/\/doi.org\/10.1016\/0304-3975(78)90020-8","journal-title":"Theor. Comput. Sci."},{"key":"4_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"112","DOI":"10.1007\/978-3-319-11439-2_9","volume-title":"Reachability Problems","author":"C Haase","year":"2014","unstructured":"Haase, C., Halfon, S.: Integer vector addition systems with states. In: Ouaknine, J., Potapov, I., Worrell, J. (eds.) RP 2014. LNCS, vol. 8762, pp. 112\u2013124. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-11439-2_9"},{"key":"4_CR14","doi-asserted-by":"publisher","unstructured":"Haase, C., Zetzsche, G.: Presburger arithmetic with stars, rational subsets of graph groups, and nested zero tests. In: Proceeding of the 34th Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS 2019), pp. 1\u201314. IEEE (2019). https:\/\/doi.org\/10.1109\/LICS.2019.8785850","DOI":"10.1109\/LICS.2019.8785850"},{"key":"4_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"743","DOI":"10.1007\/978-3-642-22110-1_60","volume-title":"Computer Aided Verification","author":"M Hague","year":"2011","unstructured":"Hague, M., Lin, A.W.: Model checking recursive programs with numeric data types. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 743\u2013759. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_60"},{"issue":"1","key":"4_CR16","doi-asserted-by":"publisher","first-page":"116","DOI":"10.1145\/322047.322058","volume":"25","author":"OH Ibarra","year":"1978","unstructured":"Ibarra, O.H.: Reversal-bounded multicounter machines and their decision problems. J. ACM 25(1), 116\u2013133 (1978). https:\/\/doi.org\/10.1145\/322047.322058","journal-title":"J. ACM"},{"issue":"3","key":"4_CR17","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1016\/0304-3975(76)90081-5","volume":"2","author":"OH Ibarra","year":"1976","unstructured":"Ibarra, O.H., Sahni, S.K., Kim, C.E.: Finite automata with multiplication. Theoret. Comput. Sci. 2(3), 271\u2013294 (1976). https:\/\/doi.org\/10.1016\/0304-3975(76)90081-5","journal-title":"Theoret. Comput. Sci."},{"key":"4_CR18","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1080\/00927870802243580","volume":"37","author":"M Kambites","year":"2009","unstructured":"Kambites, M.: Formal languages and groups as memory. Comm. Algebra 37, 193\u2013208 (2009). https:\/\/doi.org\/10.1080\/00927870802243580","journal-title":"Comm. Algebra"},{"key":"4_CR19","doi-asserted-by":"publisher","first-page":"622","DOI":"10.1016\/j.jalgebra.2006.05.020","volume":"309","author":"M Kambites","year":"2007","unstructured":"Kambites, M., Silva, P.V., Steinberg, B.: On the rational subset problem for groups. J. Algebra 309, 622\u2013639 (2007). https:\/\/doi.org\/10.1016\/j.jalgebra.2006.05.020","journal-title":"J. Algebra"},{"key":"4_CR20","doi-asserted-by":"publisher","unstructured":"Leroux, J., Schmitz, S.: Reachability in vector addition systems is primitive-recursive in fixed dimension. In: Proceeding of the 34th Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS 2019), pp. 1\u201313. IEEE (2019). https:\/\/doi.org\/10.1109\/LICS.2019.8785796","DOI":"10.1109\/LICS.2019.8785796"},{"key":"4_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"324","DOI":"10.1007\/978-3-662-47666-6_26","volume-title":"Automata, Languages, and Programming","author":"J Leroux","year":"2015","unstructured":"Leroux, J., Sutre, G., Totzke, P.: On the coverability problem for pushdown vector addition systems in one dimension. In: Halld\u00f3rsson, M.M., Iwama, K., Kobayashi, N., Speckmann, B. (eds.) ICALP 2015. LNCS, vol. 9135, pp. 324\u2013336. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-47666-6_26"},{"issue":"2","key":"4_CR22","doi-asserted-by":"publisher","first-page":"728","DOI":"10.1016\/j.jalgebra.2007.08.025","volume":"320","author":"M Lohrey","year":"2008","unstructured":"Lohrey, M., Steinberg, B.: The submonoid and rational subset membership problems for graph groups. J. Algebra 320(2), 728\u2013755 (2008)","journal-title":"J. Algebra"},{"key":"4_CR23","doi-asserted-by":"publisher","unstructured":"Lu, S., Park, S., Seo, E., Zhou, Y.: Learning from mistakes: A comprehensive study on real world concurrency bug characteristics. In: Proceedings of the 13th International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS 2008), pp. 329\u2013339. ACM (2008). https:\/\/doi.org\/10.1145\/1346281.1346323","DOI":"10.1145\/1346281.1346323"},{"issue":"1\u20133","key":"4_CR24","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1016\/S0304-3975(02)00646-1","volume":"297","author":"R Mayr","year":"2003","unstructured":"Mayr, R.: Undecidable problems in unreliable computations. Theoret. Comput. Sci. 297(1\u20133), 337\u2013354 (2003). https:\/\/doi.org\/10.1016\/S0304-3975(02)00646-1","journal-title":"Theoret. Comput. Sci."},{"key":"4_CR25","doi-asserted-by":"publisher","unstructured":"Meyer, R., Muskalla, S., Zetzsche, G.: Bounded context switching for valence systems. In: Proceeding of the 29th International Conference on Concurrency Theory (CONCUR 2018). LIPIcs, vol. 118, pp. 12:1\u201312:18. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2018). https:\/\/doi.org\/10.4230\/LIPIcs.CONCUR.2018.12","DOI":"10.4230\/LIPIcs.CONCUR.2018.12"},{"issue":"3","key":"4_CR26","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1016\/S0166-218X(00)00200-6","volume":"108","author":"V Mitrana","year":"2001","unstructured":"Mitrana, V., Stiebe, R.: Extended finite automata over groups. Discret. Appl. Math. 108(3), 287\u2013300 (2001). https:\/\/doi.org\/10.1016\/S0166-218X(00)00200-6","journal-title":"Discret. Appl. Math."},{"key":"4_CR27","doi-asserted-by":"publisher","unstructured":"Musuvathi, M., Qadeer, S.: Iterative context bounding for systematic testing of multithreaded programs. In: Proceedings of the 2007 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2007), pp. 446\u2013455. ACM (2007). https:\/\/doi.org\/10.1145\/1273442.1250785","DOI":"10.1145\/1273442.1250785"},{"key":"4_CR28","doi-asserted-by":"publisher","unstructured":"Ong, L.: Higher-order model checking: an overview. In: Proceeding of the 30th Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS 2015), pp. 1\u201315. IEEE Computer Society (2015). https:\/\/doi.org\/10.1109\/LICS.2015.9","DOI":"10.1109\/LICS.2015.9"},{"key":"4_CR29","first-page":"911","volume":"25","author":"G P\u0103un","year":"1980","unstructured":"P\u0103un, G.: A new generative device: Valence grammars. Rev. Roumaine Math. Pures Appl. 25, 911\u2013924 (1980)","journal-title":"Rev. Roumaine Math. Pures Appl."},{"key":"4_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"268","DOI":"10.1007\/978-3-540-70545-1_25","volume-title":"Computer Aided Verification","author":"R Piskac","year":"2008","unstructured":"Piskac, R., Kuncak, V.: Linear arithmetic with stars. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 268\u2013280. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-70545-1_25"},{"key":"4_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1007\/978-3-540-31980-1_7","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S Qadeer","year":"2005","unstructured":"Qadeer, S., Rehof, J.: Context-bounded model checking of concurrent software. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 93\u2013107. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/978-3-540-31980-1_7"},{"issue":"2","key":"4_CR32","doi-asserted-by":"publisher","first-page":"416","DOI":"10.1145\/349214.349241","volume":"22","author":"G Ramalingam","year":"2000","unstructured":"Ramalingam, G.: Context-sensitive synchronization-sensitive analysis is undecidable. ACM Transactions on Programming languages and Systems (TOPLAS) 22(2), 416\u2013430 (2000). https:\/\/doi.org\/10.1145\/349214.349241","journal-title":"ACM Transactions on Programming languages and Systems (TOPLAS)"},{"key":"4_CR33","first-page":"155","volume":"37","author":"V Red\u2019ko","year":"1980","unstructured":"Red\u2019ko, V., Lisovik, L.: Regular events in semigroups. Probl. Cybern. 37, 155\u2013184 (1980). in Russian","journal-title":"Probl. Cybern."},{"key":"4_CR34","doi-asserted-by":"publisher","unstructured":"Shetty, A.K., Krishna, S.N., Zetzsche, G.: Scope-bounded reachability in valence systems. In: Proceeding of the 32nd International Conference on Concurrency Theory (CONCUR 2021). LIPIcs, vol. 203, pp. 29:1\u201329:19. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2021). https:\/\/doi.org\/10.4230\/LIPIcs.CONCUR.2021.29","DOI":"10.4230\/LIPIcs.CONCUR.2021.29"},{"key":"4_CR35","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2020.104588","volume":"275","author":"SL Torre","year":"2020","unstructured":"Torre, S.L., Napoli, M., Parlato, G.: Reachability of scope-bounded multistack pushdown systems. Inf. Comput. 275, 104588 (2020). https:\/\/doi.org\/10.1016\/j.ic.2020.104588","journal-title":"Inf. Comput."},{"key":"4_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"434","DOI":"10.1007\/978-3-642-39212-2_39","volume-title":"Automata, Languages, and Programming","author":"G Zetzsche","year":"2013","unstructured":"Zetzsche, G.: Silent transitions in automata with storage. In: Fomin, F.V., Freivalds, R., Kwiatkowska, M., Peleg, D. (eds.) ICALP 2013. LNCS, vol. 7966, pp. 434\u2013445. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39212-2_39"},{"key":"4_CR37","unstructured":"Zetzsche, G.: Monoids as Storage Mechanisms. Ph.D. Thesis, Technische Universit\u00e4t Kaiserslautern (2016). https:\/\/kluedo.ub.uni-kl.de\/frontdoor\/index\/index\/docId\/4400"},{"key":"4_CR38","doi-asserted-by":"publisher","first-page":"104583","DOI":"10.1016\/j.ic.2020.104583","volume":"277","author":"G Zetzsche","year":"2021","unstructured":"Zetzsche, G.: The emptiness problem for valence automata over graph monoids. Inf. Comput. 277, 104583 (2021). https:\/\/doi.org\/10.1016\/j.ic.2020.104583","journal-title":"Inf. Comput."}],"container-title":["Lecture Notes in Computer Science","Reachability Problems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-89716-1_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,10,25]],"date-time":"2021-10-25T09:09:55Z","timestamp":1635152995000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-89716-1_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030897154","9783030897161"],"references-count":38,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-89716-1_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"22 October 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"RP","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Reachability Problems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Liverpool","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"United Kingdom","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25 October 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 October 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"15","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"rp2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/rp2021.csc.liv.ac.uk\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}