{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,11]],"date-time":"2025-06-11T04:12:40Z","timestamp":1749615160533,"version":"3.41.0"},"publisher-location":"Cham","reference-count":34,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319459936"},{"type":"electronic","value":"9783319459943"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-319-45994-3_3","type":"book-chapter","created":{"date-parts":[[2016,9,12]],"date-time":"2016-09-12T09:41:04Z","timestamp":1473673264000},"page":"36-50","source":"Crossref","is-referenced-by-count":1,"title":["On the Complexity of Resource-Bounded Logics"],"prefix":"10.1007","author":[{"given":"Natasha","family":"Alechina","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Nils","family":"Bulling","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Stephane","family":"Demri","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Brian","family":"Logan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,9,13]]},"reference":[{"key":"3_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"106","DOI":"10.1007\/978-3-642-40184-8_9","volume-title":"CONCUR 2013 \u2013 Concurrency Theory","author":"PA Abdulla","year":"2013","unstructured":"Abdulla, P.A., Mayr, R., Sangnier, A., Sproston, J.: Solving parity games on integer vectors. In: D\u2019Argenio, P.R., Melgratti, H. (eds.) CONCUR 2013 \u2013 Concurrency Theory. LNCS, vol. 8052, pp. 106\u2013120. Springer, Heidelberg (2013)"},{"key":"3_CR2","unstructured":"Alechina, N., Bulling, N., Logan, B., Nguyen, H.: On the boundary of (un)decidability: decidable model-checking for a fragment of resource agent logic. In: IJCAI 2015, pp. 1494\u20131501. AAAI Press (2015)"},{"key":"3_CR3","unstructured":"Alechina, N., Logan, B., Nguyen, H., Raimondi, F.: Decidable model-checking for a resource logic with production of resources. In: ECAI 2014, pp. 9\u201314 (2014)"},{"key":"3_CR4","unstructured":"Alechina, N., Logan, B., Nguyen, H., Raimondi, F.: Technical report: model-checking for resource-bounded ATL with production and consumption of resources. CoRR abs\/1504.06766 (2015)"},{"issue":"5","key":"3_CR5","doi-asserted-by":"crossref","first-page":"672","DOI":"10.1145\/585265.585270","volume":"49","author":"R Alur","year":"2002","unstructured":"Alur, R., Henzinger, T., Kupferman, O.: Alternating-time temporal logic. JACM 49(5), 672\u2013713 (2002)","journal-title":"JACM"},{"key":"3_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"39","DOI":"10.1007\/978-3-642-32940-1_5","volume-title":"CONCUR 2012 \u2013 Concurrency Theory","author":"B B\u00e9rard","year":"2012","unstructured":"B\u00e9rard, B., Haddad, S., Sassolas, M., Sznajder, N.: Concurrent games on VASS with inhibition. In: Koutny, M., Ulidowski, I. (eds.) CONCUR 2012. LNCS, vol. 7454, pp. 39\u201352. Springer, Heidelberg (2012)"},{"key":"3_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"108","DOI":"10.1007\/978-3-642-22993-0_13","volume-title":"Mathematical Foundations of Computer Science 2011","author":"M Blockelet","year":"2011","unstructured":"Blockelet, M., Schmitz, S.: Model checking coverability graphs of vector addition systems. In: Murlak, F., Sankowski, P. (eds.) MFCS 2011. LNCS, vol. 6907, pp. 108\u2013119. Springer, Heidelberg (2011)"},{"key":"3_CR8","doi-asserted-by":"crossref","unstructured":"Blondin, M., Finkel, A., G\u00f6ller, S., Haase, C., McKenzie, P.: Reachability in two-dimensional vector addition systems with states is PSPACE-complete. In: LICS 2015, pp. 32\u201343. ACM Press (2015)","DOI":"10.1109\/LICS.2015.14"},{"key":"3_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"478","DOI":"10.1007\/978-3-642-14162-1_40","volume-title":"Automata, Languages and Programming","author":"T Br\u00e1zdil","year":"2010","unstructured":"Br\u00e1zdil, T., Jan\u010dar, P., Ku\u010dera, A.: Reachability games on extended vector addition systems with states. In: Abramsky, S., Gavoille, C., Kirchner, C., Meyer auf der Heide, F., Spirakis, P.G. (eds.) ICALP 2010. LNCS, vol. 6199, pp. 478\u2013489. Springer, Heidelberg (2010)"},{"key":"3_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"22","DOI":"10.1007\/978-3-642-16867-3_2","volume-title":"Computational Logic in Multi-Agent Systems","author":"N Bulling","year":"2010","unstructured":"Bulling, N., Farwer, B.: Expressing properties of resource-bounded systems: the logics $${\\sf RTL}^\\text{* }$$ and $${\\sf RTL}$$ . In: Dix, J., Fisher, M., Nov\u00e1k, P. (eds.) CLIMA X. LNCS, vol. 6214, pp. 22\u201345. Springer, Heidelberg (2010)"},{"key":"3_CR11","doi-asserted-by":"crossref","unstructured":"Bulling, N., Farwer, B.: On the (un-)decidability of model-checking resource-bounded agents. In: ECAI 2010, pp. 567\u2013572 (2010)","DOI":"10.3233\/978-1-60750-606-5-567"},{"key":"3_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"640","DOI":"10.1007\/978-3-319-25524-8_47","volume-title":"PRIMA 2015: Principles and Practice of Multi-Agent Systems","author":"N Bulling","year":"2015","unstructured":"Bulling, N., Nguyen, H.: Model checking resource bounded systems with shared resources via alternating B\u00fcchi pushdown systems. In: Chen, O., Torroni, P., Villata, S., Hsu, J., Omicini, A. (eds.) PRIMA 2015. LNCS, vol. 9387, pp. 640\u2013649. Springer, Heidelberg (2015)"},{"key":"3_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"220","DOI":"10.1007\/978-3-662-44522-8_19","volume-title":"Mathematical Foundations of Computer Science 2014","author":"J-B Courtois","year":"2014","unstructured":"Courtois, J.-B., Schmitz, S.: Alternating vector addition systems with states. In: Csuhaj-Varj\u00fa, E., Dietzfelbinger, M., \u00c9sik, Z. (eds.) MFCS 2014, Part I. LNCS, vol. 8634, pp. 220\u2013231. Springer, Heidelberg (2014)"},{"issue":"5","key":"3_CR14","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"},{"issue":"1","key":"3_CR15","first-page":"23","volume":"79","author":"S Demri","year":"2013","unstructured":"Demri, S., Jurdzi\u0144ski, M., Lachish, O., Lazi\u0107, R.: The covering and boundedness problems for branching vector addition systems. JCSS 79(1), 23\u201338 (2013)","journal-title":"JCSS"},{"key":"3_CR16","doi-asserted-by":"crossref","unstructured":"Emerson, A.: Temporal and modal logic. In: Handbook of Theoretical Computer Science, pp. 996\u20131072. Elsevier (1990)","DOI":"10.1016\/B978-0-444-88074-1.50021-4"},{"key":"3_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"115","DOI":"10.1007\/BFb0017477","volume-title":"Trees in Algebra and Programming \u2013 CAAP 1994","author":"J Esparza","year":"1994","unstructured":"Esparza, J.: On the decidability of model checking for several $$\\mu $$ -calculi and Petri nets. In: Tison, J. (ed.) ICALP 1994. LNCS, vol. 787, pp. 115\u2013129. Springer, Heidelberg (1994)"},{"key":"3_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"374","DOI":"10.1007\/3-540-65306-6_20","volume-title":"Advances in Petri Nets 1998","author":"J Esparza","year":"1998","unstructured":"Esparza, J.: Decidability and complexity of Petri net problems - an introduction. In: Reisig, W., Rozenberg, G. (eds.) Advances in Petri Nets 1998. LNCS, vol. 1491, pp. 374\u2013428. Springer, Heidelberg (1998)"},{"issue":"3","key":"3_CR19","doi-asserted-by":"crossref","first-page":"884","DOI":"10.1137\/120876435","volume":"42","author":"S G\u00f6ller","year":"2013","unstructured":"G\u00f6ller, S., Lohrey, M.: Branching-time model checking of one-counter processes and timed automata. SIAM J. Comput. 42(3), 884\u2013923 (2013)","journal-title":"SIAM J. Comput."},{"key":"3_CR20","unstructured":"Haase, C.: On the complexity of model checking counter automata. Ph.D. thesis, University of Oxford (2012)"},{"key":"3_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"102","DOI":"10.1007\/3-540-63139-9_32","volume-title":"Application and Theory of Petri Nets 1997","author":"P Habermehl","year":"1997","unstructured":"Habermehl, P.: On the complexity of the linear-time mu-calculus for Petri nets. In: Az\u00e9ma, P., Balbo, G. (eds.) Application and Theory of Petri Nets 1997. LNCS, vol. 1248, pp. 102\u2013116. Springer, Heidelberg (1997)"},{"key":"3_CR22","doi-asserted-by":"crossref","first-page":"305","DOI":"10.1016\/0304-3975(89)90053-4","volume":"64","author":"R Howell","year":"1989","unstructured":"Howell, R., Rosier, L.: Problems concerning fairness and temporal logic for conflict-free Petri nets. TCS 64, 305\u2013329 (1989)","journal-title":"TCS"},{"issue":"1","key":"3_CR23","doi-asserted-by":"crossref","first-page":"71","DOI":"10.1016\/0304-3975(90)90006-4","volume":"74","author":"P Jan\u010dar","year":"1990","unstructured":"Jan\u010dar, P.: Decidability of a temporal logic problem for Petri nets. TCS 74(1), 71\u201393 (1990)","journal-title":"TCS"},{"key":"3_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"50","DOI":"10.1007\/978-3-319-24537-9_6","volume-title":"Reachability Problems","author":"P Jan\u010dar","year":"2015","unstructured":"Jan\u010dar, P.: On reachability-related games on vector addition systems with states. In: Boja\u0144czyk, M., Lasota, S., Potapov, I. (eds.) RP 2015. LNCS, vol. 9328, pp. 50\u201362. Springer, Heidelberg (2015)"},{"key":"3_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"244","DOI":"10.1007\/978-3-642-39698-4_15","volume-title":"Theories of Programming and Formal Methods","author":"L Juhl","year":"2013","unstructured":"Juhl, L., Larsen, K., Raskin, J.-F.: Optimal bounds for multiweighted and parametrised energy games. In: Liu, Z., Woodcock, J., Zhu, H. (eds.) Theories of Programming and Formal Methods. LNCS, vol. 8051, pp. 244\u2013255. Springer, Heidelberg (2013)"},{"key":"3_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"260","DOI":"10.1007\/978-3-662-47666-6_21","volume-title":"Automata, Languages, and Programming","author":"M Jurdzi\u0144ski","year":"2015","unstructured":"Jurdzi\u0144ski, M., Lazi\u0107, R., Schmitz, S.: Fixed-dimensional energy games are in pseudo-polynomial time. In: Halld\u00f3rsson, M.M., Iwama, K., Kobayashi, N., Speckmann, B. (eds.) ICALP 2015. LNCS, vol. 9135, pp. 260\u2013272. Springer, Heidelberg (2015)"},{"issue":"2","key":"3_CR27","first-page":"147","volume":"3","author":"R Karp","year":"1969","unstructured":"Karp, R., Miller, R.: Parallel program schemata. JCSS 3(2), 147\u2013195 (1969)","journal-title":"JCSS"},{"key":"3_CR28","unstructured":"Lipton, R.: The reachability problem requires exponential space. Technical Report 62, Department of Computer Science, Yale University (1976)"},{"key":"3_CR29","first-page":"215","volume":"278","author":"DD Monica","year":"2011","unstructured":"Monica, D.D., Napoli, M., Parente, M.: On a logic for coalitional games with priced-resource agents. ENTCS 278, 215\u2013228 (2011)","journal-title":"ENTCS"},{"issue":"2","key":"3_CR30","doi-asserted-by":"crossref","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)","journal-title":"TCS"},{"issue":"6","key":"3_CR31","first-page":"69","volume":"128","author":"J-F Raskin","year":"2005","unstructured":"Raskin, J.-F., Samuelides, M., Begin, L.V.: Games for counting abstractions. ENTCS 128(6), 69\u201385 (2005)","journal-title":"ENTCS"},{"key":"3_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"337","DOI":"10.1007\/11690634_23","volume-title":"Foundations of Software Science and Computation Structures","author":"O Serre","year":"2006","unstructured":"Serre, O.: Parity games played on transition graphs of one-counter processes. In: Aceto, L., Ing\u00f3lfsd\u00f3ttir, A. (eds.) FOSSACS 2006. LNCS, vol. 3921, pp. 337\u2013351. Springer, Heidelberg (2006)"},{"key":"3_CR33","doi-asserted-by":"crossref","first-page":"217","DOI":"10.46298\/dmtcs.350","volume":"7","author":"K Verma","year":"2005","unstructured":"Verma, K., Goubault-Larrecq, J.: Karp-miller trees for a branching extension of VASS. Discrete Math. Theor. Comput. Sci. 7, 217\u2013230 (2005)","journal-title":"Discrete Math. Theor. Comput. Sci."},{"key":"3_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"361","DOI":"10.1007\/978-3-319-24953-7_27","volume-title":"Automated Technology for Verification and Analysis","author":"S Vester","year":"2015","unstructured":"Vester, S.: On the complexity of model-checking branching and alternating-time temporallogics in one-counter systems. In: Finkbeiner, B., Pu, G., Zhang, L. (eds.) ATVA 2015. LNCS, vol. 9364, pp. 361\u2013377. Springer, Heidelberg (2015)"}],"container-title":["Lecture Notes in Computer Science","Reachability Problems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-45994-3_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,10]],"date-time":"2025-06-10T18:11:25Z","timestamp":1749579085000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-45994-3_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319459936","9783319459943"],"references-count":34,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-45994-3_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]}}}