{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,31]],"date-time":"2025-05-31T04:15:18Z","timestamp":1748664918857,"version":"3.41.0"},"publisher-location":"Cham","reference-count":16,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319255231"},{"type":"electronic","value":"9783319255248"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"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":[[2015]]},"DOI":"10.1007\/978-3-319-25524-8_47","type":"book-chapter","created":{"date-parts":[[2015,10,21]],"date-time":"2015-10-21T22:57:56Z","timestamp":1445468276000},"page":"640-649","source":"Crossref","is-referenced-by-count":5,"title":["Model Checking Resource Bounded Systems with Shared Resources via Alternating B\u00fcchi Pushdown Systems"],"prefix":"10.1007","author":[{"given":"Nils","family":"Bulling","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hoang Nga","family":"Nguyen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2015,11,28]]},"reference":[{"key":"47_CR1","unstructured":"Alechina, N., Logan, B., Nguyen, H.N., Raimondi, F.: Decidable model-checking for a resource logic with production of resources. In: Proceedings of the 21st European Conference on Artificial Intelligence (ECAI-2014), pp. 9\u201314. ECCAI. IOS Press (2014)"},{"key":"47_CR2","unstructured":"Alechina, N., Logan, B., Nguyen, H.N., Rakib, A.: Resource-bounded alternating-time temporal logic. In: Proceedings of the 9th International Conference on Autonomous Agents and Multiagent Systems (AAMAS 2010), pp. 481\u2013488. IFAAMAS (2010)"},{"key":"47_CR3","unstructured":"Alechina, N., Bulling, N., Logan, B., Nguyen, H.N.: On the boundary of (un)decidability: decidable model-checking for a fragment of resource agent logic. In: Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence, IJCAI 2015, Buenos Aires, Argentina, 25\u201331 July 2015, pp. 1494\u20131501 (2015)"},{"issue":"5","key":"47_CR4","doi-asserted-by":"publisher","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. Journal of the ACM 49(5), 672\u2013713 (2002)","journal-title":"Journal of the ACM"},{"key":"47_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1007\/3-540-63141-0_10","volume-title":"CONCUR\u201997: Concurrency Theory","author":"A Bouajjani","year":"1997","unstructured":"Bouajjani, A., Esparza, J., Maler, O.: Reachability analysis of pushdown automata: application to model-checking. In: Mazurkiewicz, A., Winkowski, J. (eds.) CONCUR 1997. LNCS, vol. 1243, pp. 135\u2013150. Springer, Heidelberg (1997)"},{"issue":"1","key":"47_CR6","doi-asserted-by":"publisher","first-page":"286","DOI":"10.1016\/j.tcs.2007.03.049","volume":"379","author":"L Bozzelli","year":"2007","unstructured":"Bozzelli, L.: Complexity results on branching-time pushdown model checking. Theoretical Computer Science 379(1), 286\u2013297 (2007)","journal-title":"Theoretical Computer Science"},{"key":"47_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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}}^{*}$$ and $${\\sf {RTL}}$$ . In: Dix, J., Fisher, M., Nov\u00e1k, P. (eds.) CLIMA X. LNCS, vol. 6214, pp. 22\u201345. Springer, Heidelberg (2010)"},{"key":"47_CR8","doi-asserted-by":"crossref","unstructured":"Bulling, N., Farwer, B.: On the (un-)decidability of model checking resource-bounded agents. In: Proceedings of the 19th European Conference on Artificial Intelligence (ECAI 2010), vol. 215, pp. 567\u2013572. IOS Press (2010)","DOI":"10.3233\/978-1-60750-606-5-567"},{"key":"47_CR9","doi-asserted-by":"crossref","unstructured":"Bulling, N., Nguyen, H.N.: Model checking resource bounded systems with shared resources via alternating B\u00fcchi pushdown systems. Technical report. ArXiv e-prints (2015)","DOI":"10.1007\/978-3-319-25524-8_47"},{"key":"47_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"704","DOI":"10.1007\/3-540-45465-9_60","volume-title":"Automata, Languages and Programming","author":"T Cachat","year":"2002","unstructured":"Cachat, T.: Symbolic strategy synthesis for games on pushdown graphs. In: Widmayer, P., Triguero, F., Morales, R., Hennessy, M., Eidenbenz, S., Conejo, R. (eds.) ICALP 2002. LNCS, vol. 2380, p. 704. Springer, Heidelberg (2002)"},{"key":"47_CR11","unstructured":"Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press (1999)"},{"key":"47_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/BFb0025774","volume-title":"Logics of Programs","author":"EM Clarke","year":"1981","unstructured":"Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching time temporal logic. In: Kozen, D. (ed.) Logics of Programs. LNCS, vol. 131, pp. 52\u201371. Springer, Heidelberg (1981)"},{"key":"47_CR13","doi-asserted-by":"crossref","unstructured":"Della Monica, D., Napoli, M., Parente, M.: Model checking coalitional games in shortage resource scenarios. In: Proceedings of the 4th International Symposium on Games, Automata, Logics and Formal Verification (GandALF 2013). EPTCS, vol. 119, pp. 240\u2013255 (2013)","DOI":"10.4204\/EPTCS.119.20"},{"key":"47_CR14","unstructured":"Hopcroft, J.E., Ullman, J.D.: Introduction to Automata Theory, Languages, and Computation. Addison-Wesley (1979)"},{"key":"47_CR15","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1016\/j.tcs.2014.07.001","volume":"549","author":"F Song","year":"2014","unstructured":"Song, F., Touili, T.: Efficient CTL model-checking for pushdown systems. Theoretical Computer Science 549, 127\u2013145 (2014)","journal-title":"Theoretical Computer Science"},{"key":"47_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"141","DOI":"10.1007\/11901914_13","volume-title":"Automated Technology for Verification and Analysis","author":"D Suwimonteerabuth","year":"2006","unstructured":"Suwimonteerabuth, D., Schwoon, S., Esparza, J.: Efficient algorithms for alternating pushdown systems with an application to the computation of certificate chains. In: Graf, S., Zhang, W. (eds.) ATVA 2006. LNCS, vol. 4218, pp. 141\u2013153. Springer, Heidelberg (2006)"}],"container-title":["Lecture Notes in Computer Science","PRIMA 2015: Principles and Practice of Multi-Agent Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-25524-8_47","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,31]],"date-time":"2025-05-31T02:59:22Z","timestamp":1748660362000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-25524-8_47"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319255231","9783319255248"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-25524-8_47","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]}}}