{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,4]],"date-time":"2025-11-04T21:28:15Z","timestamp":1762291695417,"version":"build-2065373602"},"publisher-location":"Cham","reference-count":46,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032095237","type":"print"},{"value":"9783032095244","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,11,5]],"date-time":"2025-11-05T00:00:00Z","timestamp":1762300800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,11,5]],"date-time":"2025-11-05T00:00:00Z","timestamp":1762300800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"DOI":"10.1007\/978-3-032-09524-4_10","type":"book-chapter","created":{"date-parts":[[2025,11,4]],"date-time":"2025-11-04T21:14:05Z","timestamp":1762290845000},"page":"140-155","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Knowing-How Reasoning with\u00a0Budgets Recasted: Universal Reachability Problem on\u00a0VASS"],"prefix":"10.1007","author":[{"given":"St\u00e9phane","family":"Demri","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Laurent","family":"Doyen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Raul","family":"Fervari","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,11,5]]},"reference":[{"key":"10_CR1","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1016\/j.tcs.2018.01.019","volume":"750","author":"N Alechina","year":"2018","unstructured":"Alechina, N., Bulling, N., Demri, S., Logan, B.: On the complexity of resource-bounded logics. TCS 750, 69\u2013100 (2018). https:\/\/doi.org\/10.1016\/j.tcs.2018.01.019","journal-title":"TCS"},{"key":"10_CR2","doi-asserted-by":"publisher","first-page":"56","DOI":"10.1016\/j.artint.2016.12.005","volume":"245","author":"N Alechina","year":"2017","unstructured":"Alechina, N., Bulling, N., Logan, B., Nguyen, H.: The virtues of idleness: a decidable fragment of resource agent logic. Artif. Intell. 245, 56\u201385 (2017). https:\/\/doi.org\/10.1016\/j.artint.2016.12.005","journal-title":"Artif. Intell."},{"key":"10_CR3","doi-asserted-by":"publisher","unstructured":"Areces, C., Cassano, V., Castro, P., Fervari, R., Saravia, A.R.: How easy it is to know how: an upper bound for the satisfiability problem. In: JELIA 2023. LNCS, vol. 14281, pp. 405\u2013419. Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-43619-2_28","DOI":"10.1007\/978-3-031-43619-2_28"},{"key":"10_CR4","doi-asserted-by":"crossref","unstructured":"Blockelet, M., Schmitz, S.: Model-checking coverability graphs of vector addition systems. In: MFCS 2011, LNCS, vol.\u00a06907, pp. 108\u2013119. Springer (2011)","DOI":"10.1007\/978-3-642-22993-0_13"},{"issue":"4","key":"10_CR5","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.: Two-variable logic on data words. ACM Trans. Comput. Log. 12(4), 27 (2011)","journal-title":"ACM Trans. Comput. Log."},{"key":"10_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1007\/978-3-540-85778-5_4","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"P Bouyer","year":"2008","unstructured":"Bouyer, P., Fahrenberg, U., Larsen, K.G., Markey, N., Srba, J.: Infinite runs in weighted timed automata with energy constraints. In: Cassez, F., Jard, C. (eds.) FORMATS 2008. LNCS, vol. 5215, pp. 33\u201347. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-85778-5_4"},{"key":"10_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"96","DOI":"10.1007\/978-3-642-24288-5_10","volume-title":"Reachability Problems","author":"L Bozzelli","year":"2011","unstructured":"Bozzelli, L., Ganty, P.: Complexity analysis of the backward coverability algorithm for VASS. In: Delzanno, G., Potapov, I. (eds.) RP 2011. LNCS, vol. 6945, pp. 96\u2013109. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-24288-5_10"},{"issue":"1","key":"10_CR8","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s10458-021-09531-9","volume":"36","author":"N Bulling","year":"2021","unstructured":"Bulling, N., Goranko, V.: Combining quantitative and qualitative reasoning in concurrent multi-player games. Auton. Agent. Multi-Agent Syst. 36(1), 1\u201333 (2021). https:\/\/doi.org\/10.1007\/s10458-021-09531-9","journal-title":"Auton. Agent. Multi-Agent Syst."},{"key":"10_CR9","doi-asserted-by":"crossref","unstructured":"Cao, R., Naumov, P.: Budget-constrained dynamics in multiagent systems. In: IJCAI 2017, pp. 915\u2013921. ijcai.org (2017). https:\/\/www.ijcai.org\/proceedings\/2017\/0127.pdf","DOI":"10.24963\/ijcai.2017\/127"},{"key":"10_CR10","doi-asserted-by":"crossref","unstructured":"Cardoza, E., Lipton, R., Meyer, A.: Exponential space complete problems for petri nets and commutative semigroups: Preliminary report. In: STOC 1976, pp. 50\u201354. ACM (1976)","DOI":"10.1145\/800113.803630"},{"key":"10_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"367","DOI":"10.1007\/978-3-319-63121-9_18","volume-title":"Models, Algorithms, Logics and Tools","author":"K Chatterjee","year":"2017","unstructured":"Chatterjee, K., Doyen, L., Henzinger, T.A.: The cost of exactness in quantitative reachability. In: Aceto, L., Bacci, G., Bacci, G., Ing\u00f3lfsd\u00f3ttir, A., Legay, A., Mardare, R. (eds.) Models, Algorithms, Logics and Tools. LNCS, vol. 10460, pp. 367\u2013381. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63121-9_18"},{"issue":"1\u20132","key":"10_CR12","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1016\/S0004-3702(02)00374-0","volume":"147","author":"A Cimatti","year":"2003","unstructured":"Cimatti, A., Pistore, M., Roveri, M., Traverso, P.: Weak, strong, and strong cyclic planning via symbolic model checking. Artif. Intell. 147(1\u20132), 35\u201384 (2003)","journal-title":"Artif. Intell."},{"key":"10_CR13","doi-asserted-by":"crossref","unstructured":"Czerwinski, W., Orlikowski, L.: Reachability in vector addition systems is Ackermann-complete. In: STOC 2021, pp. 1229\u20131240. IEEE (2021)","DOI":"10.1109\/FOCS52979.2021.00120"},{"key":"10_CR14","unstructured":"David, C.: Analyse de XML avec donn\u00e9es non-born\u00e9es. Ph.D. thesis, LIAFA, Universit\u00e9 Paris VII (2009)"},{"key":"10_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"260","DOI":"10.1007\/978-3-642-15205-4_22","volume-title":"Computer Science Logic","author":"A Degorre","year":"2010","unstructured":"Degorre, A., Doyen, L., Gentilini, R., Raskin, J.-F., Toru\u0144czyk, S.: Energy and mean-payoff games with imperfect information. In: Dawar, A., Veith, H. (eds.) CSL 2010. LNCS, vol. 6247, pp. 260\u2013274. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-15205-4_22"},{"key":"10_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"313","DOI":"10.1007\/978-3-642-15375-4_22","volume-title":"CONCUR 2010 - Concurrency Theory","author":"G Delzanno","year":"2010","unstructured":"Delzanno, G., Sangnier, A., Zavattaro, G.: Parameterized verification of ad hoc networks. In: Gastin, P., Laroussinie, F. (eds.) CONCUR 2010. LNCS, vol. 6269, pp. 313\u2013327. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-15375-4_22"},{"issue":"5","key":"10_CR17","first-page":"689","volume":"79","author":"S Demri","year":"2013","unstructured":"Demri, S.: On selective unboundedness of VASS. JCSS 79(5), 689\u2013713 (2013)","journal-title":"JCSS"},{"key":"10_CR18","doi-asserted-by":"crossref","unstructured":"Demri, S., Fervari, R.: Model-checking for ability-based logics with constrained plans. In: AAAI 2023, pp. 6305\u20136312. AAAI Press (2023). https:\/\/ojs.aaai.org\/index.php\/AAAI\/article\/view\/25776","DOI":"10.1609\/aaai.v37i5.25776"},{"key":"10_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"374","DOI":"10.1007\/3-540-65306-6_20","volume-title":"Lectures on Petri Nets I: Basic Models","author":"J Esparza","year":"1998","unstructured":"Esparza, J.: Decidability and complexity of petri net problems \u2014 an introduction. In: Reisig, W., Rozenberg, G. (eds.) ACPN 1996. LNCS, vol. 1491, pp. 374\u2013428. Springer, Heidelberg (1998). https:\/\/doi.org\/10.1007\/3-540-65306-6_20"},{"key":"10_CR20","doi-asserted-by":"crossref","unstructured":"Figueira, D., Figueira, S., Schmitz, S., Schnoebelen, P.: Ackermannian and primitive-recursive bounds with dickson\u2019s lemma. In: LiCS 2011, pp. 269\u2013278 (2011). https:\/\/arxiv.org\/abs\/1007.2989","DOI":"10.1109\/LICS.2011.39"},{"issue":"1\u20132","key":"10_CR21","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 transitions systems everywhere! TCS 256(1\u20132), 63\u201392 (2001). https:\/\/doi.org\/10.1016\/S0304-3975(00)00102-X","journal-title":"TCS"},{"key":"10_CR22","doi-asserted-by":"publisher","first-page":"50","DOI":"10.1016\/j.tcs.2017.05.009","volume":"735","author":"P Hofman","year":"2018","unstructured":"Hofman, P., Totzke, P.: Trace inclusion for one-counter nets revisited. TCS 735, 50\u201363 (2018). https:\/\/doi.org\/10.1016\/j.tcs.2017.05.009","journal-title":"TCS"},{"key":"10_CR23","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1016\/0304-3975(79)90041-0","volume":"8","author":"J Hopcroft","year":"1979","unstructured":"Hopcroft, J., Pansiot, J.: On the reachability problem for 5-dimensional vector addition systems. TCS 8, 135\u2013159 (1979). https:\/\/doi.org\/10.1016\/0304-3975(79)90041-0","journal-title":"TCS"},{"key":"10_CR24","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). https:\/\/doi.org\/10.1007\/978-3-642-14295-6_55"},{"issue":"2","key":"10_CR25","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1016\/S0022-0000(69)80011-5","volume":"3","author":"RM Karp","year":"1969","unstructured":"Karp, R.M., Miller, R.E.: Parallel program schemata. JCSS 3(2), 147\u2013195 (1969). https:\/\/doi.org\/10.1016\/S0022-0000(69)80011-5","journal-title":"JCSS"},{"key":"10_CR26","doi-asserted-by":"crossref","unstructured":"Kosaraju, R.: Decidability of reachability in vector addition systems. In: STOC 1982, pp. 267\u2013281 (1982)","DOI":"10.1145\/800070.802201"},{"key":"10_CR27","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1016\/0304-3975(92)90173-D","volume":"99","author":"J Lambert","year":"1992","unstructured":"Lambert, J.: A structure to decide reachability in petri nets. TCS 99, 79\u2013104 (1992)","journal-title":"TCS"},{"key":"10_CR28","doi-asserted-by":"publisher","first-page":"104582","DOI":"10.1016\/j.ic.2020.104582","volume":"277","author":"R Lazi\u0107","year":"2021","unstructured":"Lazi\u0107, R., Schmitz, S.: The ideal view on Rackoff\u2019s coverability technique. Inf. Comput. 277, 104582 (2021). https:\/\/doi.org\/10.1016\/j.ic.2020.104582","journal-title":"Inf. Comput."},{"key":"10_CR29","doi-asserted-by":"crossref","unstructured":"Leroux, J.: The general vector addition system reachability problem by Presburger inductive invariants. In: LiCS 2009, pp. 4\u201313. IEEE (2009)","DOI":"10.1109\/LICS.2009.10"},{"key":"10_CR30","doi-asserted-by":"crossref","unstructured":"Leroux, J.: Vector addition system reachability problem (A short self-contained proof). In: POPL 2011, pp. 307\u2013316 (2011)","DOI":"10.1145\/1926385.1926421"},{"key":"10_CR31","doi-asserted-by":"crossref","unstructured":"Leroux, J.: The reachability problem for petri nets is not primitive recursive. In: FOCS 2021, pp. 1241\u20131252. IEEE (2021). https:\/\/arxiv.org\/abs\/2104.12695","DOI":"10.1109\/FOCS52979.2021.00121"},{"key":"10_CR32","doi-asserted-by":"crossref","unstructured":"Leroux, J., Schmitz, S.: Reachability in vector addition systems is primitive-recursive in fixed dimension. In: LiCS 2019, pp. 1\u201313. IEEE (2019)","DOI":"10.1109\/LICS.2019.8785796"},{"key":"10_CR33","unstructured":"Li, Y.: Knowing what to do: a logical approach to planning and knowing how. Ph.D. thesis, University of Groningen (2017). https:\/\/pure.rug.nl\/ws\/portalfiles\/portal\/47919164\/Complete_thesis.pdf"},{"key":"10_CR34","doi-asserted-by":"publisher","unstructured":"Li, Y., Wang, Y.: Achieving while maintaining: - a logic of knowing how with intermediate constraints. In: ICLA 2017, LNCS, vol. 10119, pp. 154\u2013167. Springer (2017). https:\/\/doi.org\/10.1007\/978-3-662-54069-5_12","DOI":"10.1007\/978-3-662-54069-5_12"},{"key":"10_CR35","unstructured":"Lipton, R.: The reachability problem requires exponential space. Technical Report\u00a062, Department of Computer Science, Yale University (1976). http:\/\/www.cs.yale.edu\/publications\/techreports\/tr63.pdf"},{"issue":"3","key":"10_CR36","doi-asserted-by":"publisher","first-page":"441","DOI":"10.1137\/0213029","volume":"13","author":"E Mayr","year":"1984","unstructured":"Mayr, E.: An algorithm for the general petri net reachability problem. SIAM J. Comput. 13(3), 441\u2013460 (1984)","journal-title":"SIAM J. Comput."},{"key":"10_CR37","unstructured":"Minsky, M.: Computation, Finite and Infinite Machines. Prentice Hall (1967)"},{"key":"10_CR38","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1016\/j.ipl.2016.10.005","volume":"118","author":"G P\u00e9rez","year":"2017","unstructured":"P\u00e9rez, G.: The fixed initial credit problem for partial-observation energy games is ack-complete. IPL 118, 91\u201399 (2017). https:\/\/doi.org\/10.1016\/j.ipl.2016.10.005","journal-title":"IPL"},{"issue":"2","key":"10_CR39","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1016\/0304-3975(78)90036-1","volume":"6","author":"C Rackoff","year":"1978","unstructured":"Rackoff, C.: The covering and boundedness problems for vector addition systems. TCS 6(2), 223\u2013231 (1978). https:\/\/doi.org\/10.1016\/0304-3975(78)90036-1","journal-title":"TCS"},{"key":"10_CR40","unstructured":"Reutenauer, C.: The mathematics of Petri nets. Masson and Prentice (1990)"},{"key":"10_CR41","unstructured":"Schmitz, S.: Algorithmic complexity of well-quasi-orders, November 2017, habilitation thesis"},{"key":"10_CR42","doi-asserted-by":"crossref","unstructured":"Schmitz, S.: Complexity hierarchies beyond elementary. ACM Trans. Comput. Theor. 8(1), 3:1\u20133:36 (2016). https:\/\/doi.org\/10.1145\/2858784","DOI":"10.1145\/2858784"},{"key":"10_CR43","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"616","DOI":"10.1007\/978-3-642-15155-2_54","volume-title":"Mathematical Foundations of Computer Science 2010","author":"P Schnoebelen","year":"2010","unstructured":"Schnoebelen, P.: Revisiting ackermann-hardness for lossy counter machines and reset petri nets. In: Hlin\u011bn\u00fd, P., Ku\u010dera, A. (eds.) MFCS 2010. LNCS, vol. 6281, pp. 616\u2013628. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-15155-2_54"},{"key":"10_CR44","doi-asserted-by":"publisher","unstructured":"Wang, Y.: A logic of knowing how. In: LORI 2015, LNCS, vol.\u00a09394, pp. 392\u2013405. Springer (2015). https:\/\/doi.org\/10.1007\/978-3-662-48561-3_32","DOI":"10.1007\/978-3-662-48561-3_32"},{"key":"10_CR45","doi-asserted-by":"publisher","unstructured":"Wang, Y.: A logic of goal-directed knowing how. Synthese 195(10), 4419\u20134439 (2018). https:\/\/doi.org\/10.1007\/s11229-016-1272-0","DOI":"10.1007\/s11229-016-1272-0"},{"key":"10_CR46","series-title":"Outstanding Contributions to Logic","doi-asserted-by":"publisher","first-page":"499","DOI":"10.1007\/978-3-319-62864-6_21","volume-title":"Jaakko Hintikka on Knowledge and Game-Theoretical Semantics","author":"Y Wang","year":"2018","unstructured":"Wang, Y.: Beyond knowing that: a new generation of epistemic logics. In: van Ditmarsch, H., Sandu, G. (eds.) Jaakko Hintikka on Knowledge and Game-Theoretical Semantics. OCL, vol. 12, pp. 499\u2013533. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-62864-6_21"}],"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-032-09524-4_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,11,4]],"date-time":"2025-11-04T21:14:07Z","timestamp":1762290847000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-09524-4_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,11,5]]},"ISBN":["9783032095237","9783032095244"],"references-count":46,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-09524-4_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,11,5]]},"assertion":[{"value":"5 November 2025","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":"Madrid","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Spain","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"1 October 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"3 October 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"19","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"rp2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/rp25.software.imdea.org\/index.html","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}