{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,4]],"date-time":"2025-06-04T04:17:28Z","timestamp":1749010648805,"version":"3.41.0"},"publisher-location":"Cham","reference-count":28,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319401881"},{"type":"electronic","value":"9783319401898"}],"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-40189-8_1","type":"book-chapter","created":{"date-parts":[[2016,6,13]],"date-time":"2016-06-13T15:34:07Z","timestamp":1465832047000},"page":"3-12","source":"Crossref","is-referenced-by-count":1,"title":["Verifying Systems of Resource-Bounded Agents"],"prefix":"10.1007","author":[{"given":"Natasha","family":"Alechina","sequence":"first","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,6,14]]},"reference":[{"unstructured":"Alechina, N., Logan, B., Nguyen, H.N., Rakib, A.: A logic for coalitions with bounded resources. In: Proceedings of the 21st International Joint Conference on Artificial Intelligence (IJCAI 2009), vol. 2, pp. 659\u2013664. IJCAI\/AAAI, AAAI Press (2009)","key":"1_CR1"},{"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":"1_CR2"},{"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: Yang, Q. (ed.) Proceedings of the 24th International Joint Conference on Artificial Intelligence (IJCAI 2015). AAAI Press, Buenos Aires, July 2015","key":"1_CR3"},{"unstructured":"Alechina, N., Dastani, M., Logan, B.: Verifying existence of resource-bounded coalition uniform strategies. In: Rossi, F. (ed.) IJCAI 2016, Proceedings of the 25th International Joint Conference on Artificial Intelligence. IJCAI\/AAAI (2016)","key":"1_CR4"},{"issue":"6","key":"1_CR5","doi-asserted-by":"crossref","first-page":"907","DOI":"10.1093\/logcom\/exq032","volume":"21","author":"N Alechina","year":"2011","unstructured":"Alechina, N., Logan, B., Nga, N.H., Rakib, A.: Logic for coalitions with bounded resources. J. Logic Comput. 21(6), 907\u2013937 (2011)","journal-title":"J. Logic Comput."},{"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. IOS Press, Prague, August 2014","key":"1_CR6"},{"unstructured":"Alechina, N., Logan, B., Nguyen, H.N., Raimondi, F.: Symbolic model-checking for oneresource RB+-ATL. In: Yang, Q. (ed.) Proceedings of the 24th International Joint Conference on Artificial Intelligence (IJCAI 2015). AAAI Press, Buenos Aires, July 2015","key":"1_CR7"},{"unstructured":"Alechina, N., Logan, B., Nguyen, H.N., Raimondi, F., Mostarda, L.: Symbolic model-checking for resource-bounded ATL. In: Proceedings of the 2015 International Conference on Autonomous Agents and Multiagent Systems, AAMAS 2015, pp. 1809\u20131810. ACM (2015)","key":"1_CR8"},{"issue":"5","key":"1_CR9","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. J. ACM 49(5), 672\u2013713 (2002)","journal-title":"J. ACM"},{"key":"1_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"521","DOI":"10.1007\/BFb0028774","volume-title":"Computer Aided Verification","author":"R Alur","year":"1998","unstructured":"Alur, R., Henzinger, T.A., Mang, F.Y.C., Qadeer, S., Rajamani, S.K., Tasiran, S.: MOCHA: modularity in model checking. In: Hu, A.J., Vardi, M.Y. (eds.) Computer Aided Verification. LNCS, vol. 1247, pp. 521\u2013525. Springer, Heidelberg (1998)"},{"unstructured":"Belardinelli, F.: Verification of non-uniform and unbounded artifact-centric systems: decidability through abstraction. In: Bazzan, A.L.C., Huhns, M.N., Lomuscio, A., Scerri, P. (eds.) International conference on Autonomous Agents and Multi-Agent Systems, AAMAS 2014, pp. 717\u2013724. IFAAMAS\/ACM (2014)","key":"1_CR11"},{"issue":"5","key":"1_CR12","doi-asserted-by":"crossref","first-page":"46","DOI":"10.1109\/MIS.2004.47","volume":"19","author":"RH Bordini","year":"2004","unstructured":"Bordini, R.H., Fisher, M., Visser, W., Wooldridge, M.: Model checking rational agents. IEEE Intell. Syst. 19(5), 46\u201352 (2004)","journal-title":"IEEE Intell. Syst."},{"issue":"2","key":"1_CR13","doi-asserted-by":"crossref","first-page":"239","DOI":"10.1007\/s10458-006-5955-7","volume":"12","author":"RH Bordini","year":"2006","unstructured":"Bordini, R.H., Fisher, M., Visser, W., Wooldridge, M.: Verifying multi-agent programs by model checking. J. Auton. Agents Multi-Agent Syst. 12(2), 239\u2013256 (2006). http:\/\/dro.dur.ac.uk\/622\/","journal-title":"J. Auton. Agents Multi-Agent Syst."},{"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). Frontiers in Artificial Intelligence and Applications, vol. 215, pp. 567\u2013572. IOS Press (2010)","key":"1_CR14","DOI":"10.3233\/978-1-60750-606-5-567"},{"doi-asserted-by":"crossref","unstructured":"Bulling, N., Farwer, B.: On the (un-)decidability of model checking resource-bounded agents. Technical report IfI-10-05, Clausthal University of Technology (2010)","key":"1_CR15","DOI":"10.3233\/978-1-60750-606-5-567"},{"key":"1_CR16","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 RTL $$^{*}$$ \u2217 and RTL. In: Fisher, M., Nov\u00e1k, P., Dix, J. (eds.) CLIMA X. LNCS, vol. 6214, pp. 22\u201345. Springer, Heidelberg (2010)"},{"doi-asserted-by":"crossref","unstructured":"Bulling, N., Goranko, V.: How to be both rich and happy: combining quantitative and qualitative strategic reasoning about multi-player games (extended abstract). In: Mogavero, F., Murano, A., Vardi, M.Y. (eds.) Proceedings 1st International Workshop on Strategic Reasoning, SR 2013. EPTCS, vol. 112, pp. 33\u201341 (2013)","key":"1_CR17","DOI":"10.4204\/EPTCS.112.8"},{"key":"1_CR18","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.N.: Model checking resource bounded systems with shared resources via alternating b\u00fcchi pushdown systems. In: Chen, Q., Torroni, P., Villata, S., Hsu, J., Omicini, A. (eds.) PRIMA 2015: Principles and Practice of Multi-Agent Systems. LNCS, vol. 9387, pp. 640\u2013649. Springer, Heidelberg (2015)"},{"issue":"2","key":"1_CR19","doi-asserted-by":"crossref","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"EM Clarke","year":"1986","unstructured":"Clarke, E.M., Emerson, E.A., Sistla, A.P.: Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Trans. Program. Lang. Syst. 8(2), 244\u2013263 (1986)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"1_CR20","doi-asserted-by":"crossref","first-page":"215","DOI":"10.1016\/j.entcs.2011.10.017","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. Electr. Notes. Theor. Comput. Sci. 278, 215\u2013228 (2011)","journal-title":"Electr. Notes. Theor. Comput. Sci."},{"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)","key":"1_CR21","DOI":"10.4204\/EPTCS.119.20"},{"issue":"1","key":"1_CR22","doi-asserted-by":"crossref","first-page":"5","DOI":"10.1007\/s10515-011-0088-x","volume":"19","author":"LA Dennis","year":"2012","unstructured":"Dennis, L.A., Fisher, M., Webster, M.P., Bordini, R.H.: Model checking agent programming languages. Autom. Softw. Eng. 19(1), 5\u201363 (2012)","journal-title":"Autom. Softw. Eng."},{"unstructured":"Dima, C., Tiplea, F.L.: Model-checking ATL under imperfect information and perfect recall semantics is undecidable. CoRR abs\/1102.4225 (2011). http:\/\/arxiv.org\/abs\/1102.4225","key":"1_CR23"},{"issue":"9","key":"1_CR24","doi-asserted-by":"crossref","first-page":"84","DOI":"10.1145\/2500468.2494558","volume":"56","author":"M Fisher","year":"2013","unstructured":"Fisher, M., Dennis, L.A., Webster, M.P.: Verifying autonomous systems. Commun. ACM 56(9), 84\u201393 (2013)","journal-title":"Commun. ACM"},{"unstructured":"Hopcroft, J.E., Ullman, J.D.: Introduction to Automata Theory. Addison-Wesley, Languages and Computation (1979)","key":"1_CR25"},{"key":"1_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"585","DOI":"10.1007\/978-3-642-22110-1_47","volume-title":"Computer Aided Verification","author":"M Kwiatkowska","year":"2011","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 585\u2013591. Springer, Heidelberg (2011)"},{"key":"1_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"682","DOI":"10.1007\/978-3-642-02658-4_55","volume-title":"Computer Aided Verification","author":"A Lomuscio","year":"2009","unstructured":"Lomuscio, A., Qu, H., Raimondi, F.: MCMAS: a model checker for the verification of multi-agent systems. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 682\u2013688. Springer, Heidelberg (2009)"},{"doi-asserted-by":"crossref","unstructured":"Shapiro, S., Lesp\u00e9rance, Y., Levesque, H.J.: The cognitive agents specification language and verification environment for multiagent systems. In: Proceedings of the First International Joint Conference on Autonomous Agents and Multiagent Systems (AAMAS 2002), pp. 19\u201326. ACM, New York (2002)","key":"1_CR28","DOI":"10.1145\/544741.544746"}],"container-title":["Lecture Notes in Computer Science","Pursuit of the Universal"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-40189-8_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,3]],"date-time":"2025-06-03T21:35:18Z","timestamp":1748986518000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-40189-8_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319401881","9783319401898"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-40189-8_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]}}}