{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,1,22]],"date-time":"2025-01-22T05:26:20Z","timestamp":1737523580117,"version":"3.33.0"},"reference-count":42,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2007,10,30]],"date-time":"2007-10-30T00:00:00Z","timestamp":1193702400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Theory Comput Syst"],"published-print":{"date-parts":[[2008,4]]},"DOI":"10.1007\/s00224-007-9080-z","type":"journal-article","created":{"date-parts":[[2007,10,29]],"date-time":"2007-10-29T15:10:24Z","timestamp":1193670624000},"page":"366-410","source":"Crossref","is-referenced-by-count":13,"title":["Model Checking Abilities of Agents: A Closer Look"],"prefix":"10.1007","volume":"42","author":[{"given":"Wojciech","family":"Jamroga","sequence":"first","affiliation":[]},{"given":"J\u00fcrgen","family":"Dix","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2007,10,30]]},"reference":[{"key":"9080_CR1","doi-asserted-by":"crossref","first-page":"100","DOI":"10.1109\/SFCS.1997.646098","volume-title":"Proceedings of the 38th Annual Symposium on Foundations of Computer Science (FOCS)","author":"R. Alur","year":"1997","unstructured":"Alur, R., Henzinger, T.A., Kupferman, O.: Alternating-time temporal logic. In Proceedings of the 38th Annual Symposium on Foundations of Computer Science (FOCS), pp.\u00a0100\u2013109. IEEE Computer Society, Los Alamitos (1997)"},{"key":"9080_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1007\/3-540-49213-5_2","volume-title":"Alternating-Time Temporal Logic","author":"R. Alur","year":"1998","unstructured":"Alur, R., Henzinger, T.A., Kupferman, O.: Alternating-Time Temporal Logic. Lecture Notes in Computer Science, vol.\u00a01536, pp.\u00a023\u201360. Springer, Berlin (1998)"},{"key":"9080_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"521","DOI":"10.1007\/BFb0028774","volume-title":"Proceedings of CAV\u201998","author":"R. Alur","year":"1998","unstructured":"Alur, R., Henzinger, T.A., Mang, F.Y.C., Qadeer, S., Rajamani, S.K., Tasiran, S.: MOCHA user manual. In: Proceedings of CAV\u201998. Lecture Notes in Computer Science, vol.\u00a01427, pp.\u00a0521\u2013525. Springer, Berlin (1998)"},{"key":"9080_CR4","first-page":"835","volume-title":"Proceedings of ICSE","author":"R. Alur","year":"2001","unstructured":"Alur, R., de Alfaro, L., Grossu, R., Henzinger, T.A., Kang, M., Kirsch, C.M., Majumdar, R., Mang, F.Y.C., Wang, B.-Y.: jMocha: a model-checking tool that exploits design structure. In Proceedings of ICSE, pp.\u00a0835\u2013836. IEEE Computer Society, Los Alamitos (2001)"},{"key":"9080_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.A., Kupferman, O.: Alternating-time temporal logic. J. ACM 49, 672\u2013713 (2002)","journal-title":"J. ACM"},{"key":"9080_CR6","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-97062-7","volume-title":"Structural Complexity I","author":"J.L. Balc\u00e1zar","year":"1988","unstructured":"Balc\u00e1zar, J.L., Diaz, J., Gabarr\u00f3, J.: Structural Complexity I. Springer, Berlin (1988)"},{"key":"9080_CR7","doi-asserted-by":"crossref","first-page":"281","DOI":"10.1016\/S0004-3702(96)00047-1","volume":"90","author":"A.L. Blum","year":"1997","unstructured":"Blum, A.L., Furst, M.L.: Fast planning through graph analysis. Artif. Intell. 90, 281\u2013300 (1997)","journal-title":"Artif. Intell."},{"issue":"2","key":"9080_CR8","doi-asserted-by":"crossref","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"E.M. 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":"9080_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"458","DOI":"10.1007\/3-540-44618-4_33","volume-title":"Proceedings of CONCUR 2000","author":"L. Alfaro de","year":"2000","unstructured":"de Alfaro, L., Henzinger, T.A., Mang, F.Y.C.: The control of synchronous systems. In: Proceedings of CONCUR 2000. Lecture Notes in Computer Science, vol.\u00a01877, pp.\u00a0458\u2013473. Springer, Berlin (2000)"},{"key":"9080_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"566","DOI":"10.1007\/3-540-44685-0_38","volume-title":"Proceedings of CONCUR 2001","author":"L. Alfaro de","year":"2001","unstructured":"de Alfaro, L., Henzinger, T.A., Mang, F.Y.C.: The control of synchronous systems, part II. In: Proceedings of CONCUR 2001. Lecture Notes in Computer Science, vol.\u00a02154, pp.\u00a0566\u2013580. Springer, Berlin (2001)"},{"key":"9080_CR11","unstructured":"Eiter, T.: Oral communication (March 2005)"},{"key":"9080_CR12","first-page":"995","volume-title":"Handbook of Theoretical Computer Science","author":"E.A. Emerson","year":"1990","unstructured":"Emerson, E.A.: Temporal and modal logic. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, vol.\u00a0B, pp.\u00a0995\u20131072. Elsevier, Amsterdam (1990)"},{"key":"9080_CR13","doi-asserted-by":"crossref","unstructured":"Emerson, E.A., Halpern, J.Y.: \u201cSometimes\u201d and \u201cnot never\u201d revisited: on branching versus linear time temporal logic. In: Proceedings of the Annual ACM Symposium on Principles of Programming Languages, pp.\u00a0151\u2013178 (1982)","DOI":"10.1145\/4904.4999"},{"issue":"1","key":"9080_CR14","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0022-0000(85)90001-7","volume":"30","author":"E.A. Emerson","year":"1985","unstructured":"Emerson, E.A., Halpern, J.Y.: Decision procedures and expressiveness in the temporal logic of branching time. J. Comput. Syst. Sci. 30(1), 1\u201324 (1985)","journal-title":"J. Comput. Syst. Sci."},{"key":"9080_CR15","first-page":"259","volume-title":"Proceedings of TARK VIII","author":"V. Goranko","year":"2001","unstructured":"Goranko, V.: Coalition games and alternating temporal logics. In: van Benthem, J. (ed.) Proceedings of TARK VIII, pp.\u00a0259\u2013272. Morgan Kaufmann, San Mateo (2001)"},{"issue":"2","key":"9080_CR16","doi-asserted-by":"crossref","first-page":"241","DOI":"10.1023\/B:SYNT.0000024915.66183.d1","volume":"139","author":"V. Goranko","year":"2004","unstructured":"Goranko, V., Jamroga, W.: Comparing semantics of logics for multi-agent systems. Synthese 139(2), 241\u2013280 (2004)","journal-title":"Synthese"},{"key":"9080_CR17","unstructured":"Jamroga, W.: Some remarks on alternating temporal epistemic logic. In: B. Dunin-Keplicz, R. Verbrugge, (eds.) In: Proceedings of Formal Approaches to Multi-Agent Systems (FAMAS 2003), pp.\u00a0133\u2013140 (2003)"},{"key":"9080_CR18","unstructured":"Jamroga, W.: Using multiple models of reality. On agents who know how to play safer. PhD thesis, University of Twente (2004)"},{"key":"9080_CR19","doi-asserted-by":"crossref","unstructured":"Jamroga, W., \u00c5gotnes, T.: Constructive knowledge: what agents can achieve under incomplete information. Technical Report IfI-05-10, Clausthal University of Technology (2005)","DOI":"10.1145\/1160633.1160672"},{"key":"9080_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"398","DOI":"10.1007\/11559221_40","volume-title":"Proceedings of CEEMAS 2005","author":"W. Jamroga","year":"2005","unstructured":"Jamroga, W., Dix, J.: Do agents make model checking explode (computationally)? In: P\u0115chouc\u0306ek, M., Petta, P., Varga, L.Z. (eds.) Proceedings of CEEMAS 2005. Lecture Notes in Computer Science, vol.\u00a03690, pp.\u00a0398\u2013407. Springer, Berlin (2005)"},{"key":"9080_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"295","DOI":"10.1007\/11560586_24","volume-title":"Proceedings of ICTCS 2005","author":"W. Jamroga","year":"2005","unstructured":"Jamroga, W., Dix, J.: Model checking strategic abilities of agents under incomplete information. In: Coppo, M., Lodi, E., Pinna, G.M. (eds.) Proceedings of ICTCS 2005, Lecture Notes in Computer Science, vol.\u00a03701, pp.\u00a0295\u2013308. Springer, Berlin (2005)"},{"key":"9080_CR22","unstructured":"Jamroga, W., Dix, J.: Turning game models turn-based for model checking properties of agents. In: Verbeeck, K., Tuyls, K., Now\u00e9, A., Manderick, B., Kuijpers, B. (eds.) Proceedings of BNAIC, pp.\u00a0143\u2013150 (2005)"},{"issue":"2\u20133","key":"9080_CR23","first-page":"185","volume":"63","author":"W. Jamroga","year":"2004","unstructured":"Jamroga, W., van der Hoek, W.: Agents that know how to play. Fundam. Inform. 63(2\u20133), 185\u2013219 (2004)","journal-title":"Fundam. Inform."},{"key":"9080_CR24","unstructured":"Jonker, G.: Feasible strategies in alternating-time temporal epistemic logic. Master thesis, University of Utrecht (2003)"},{"key":"9080_CR25","doi-asserted-by":"crossref","unstructured":"Kacprzak, M., Penczek, W.: Unbounded model checking for alternating-time temporal logic. In: Proceedings of AAMAS-04 (2004)","DOI":"10.1007\/1-4020-4094-6_9"},{"issue":"2","key":"9080_CR26","doi-asserted-by":"crossref","first-page":"312","DOI":"10.1145\/333979.333987","volume":"47","author":"O. Kupferman","year":"2000","unstructured":"Kupferman, O., Vardi, M.Y., Wolper, P.: An automata-theoretic approach to branching-time model checking. J. ACM 47(2), 312\u2013360 (2000)","journal-title":"J. ACM"},{"issue":"6","key":"9080_CR27","doi-asserted-by":"crossref","first-page":"343","DOI":"10.1016\/0020-0190(95)00053-F","volume":"54","author":"F. Laroussinie","year":"1995","unstructured":"Laroussinie, F.: About the expressive power of CTL combinators. Inf. Process. Lett. 54(6), 343\u2013345 (1995)","journal-title":"Inf. Process. Lett."},{"key":"9080_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"318","DOI":"10.1007\/3-540-45315-6_21","volume-title":"Proceedings of FoSSaCS\u201901","author":"F. Laroussinie","year":"2001","unstructured":"Laroussinie, F., Markey, N., Schnoebelen, Ph.: Model checking CTL+ and FCTL is hard. In: Proceedings of FoSSaCS\u201901. Lecture Notes in Computer Science, vol.\u00a02030, pp.\u00a0318\u2013331. Springer, Berlin (2001)"},{"key":"9080_CR29","unstructured":"Laroussinie, F., Markey, N., Oreiby, G.: Expressiveness and complexity of ATL. Technical Report LSV-06-03, CNRS & ENS Cachan, France (2006)"},{"key":"9080_CR30","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-4222-2","volume-title":"Temporal Verification of Reactive Systems: Safety","author":"Z. Manna","year":"1995","unstructured":"Manna, Z., Pnueli, A.: Temporal Verification of Reactive Systems: Safety. Springer, Berlin (1995)"},{"key":"9080_CR31","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4615-3190-6","volume-title":"Symbolic Model Checking: An Approach to the State Explosion Problem","author":"K.L. McMillan","year":"1993","unstructured":"McMillan, K.L.: Symbolic Model Checking: An Approach to the State Explosion Problem. Kluwer Academic, Dordrecht (1993)"},{"key":"9080_CR32","volume-title":"Formal Theories of the Commonsense World","author":"R.C. Moore","year":"1985","unstructured":"Moore, R.C.: A formal theory of knowledge and action. In: Hobbs, J., Moore, R.C. (eds.) Formal Theories of the Commonsense World. Ablex, Norwood (1985)"},{"key":"9080_CR33","unstructured":"Morgenstern, L.: Knowledge and the frame problem. Int. J. Expert Syst. 3(4) (1991)"},{"key":"9080_CR34","volume-title":"Computational Complexity","author":"C.H. Papadimitriou","year":"1994","unstructured":"Papadimitriou, C.H.: Computational Complexity. Addison\u2013Wesley, Reading (1994)"},{"key":"9080_CR35","doi-asserted-by":"crossref","first-page":"177","DOI":"10.2307\/2022451","volume":"53","author":"W. Quine","year":"1956","unstructured":"Quine, W.: Quantifiers and propositional attitudes. J. Philos. 53, 177\u2013187 (1956)","journal-title":"J. Philos."},{"key":"9080_CR36","doi-asserted-by":"crossref","unstructured":"Schobbens, P.Y.: Alternating-time logic with imperfect recall. Electron. Notes Theor. Comput. Sci. 85(2) (2004)","DOI":"10.1016\/S1571-0661(05)82604-0"},{"key":"9080_CR37","unstructured":"van der Hoek, W.: Formal comment on W. Jamroga\u2019s paper. Presented at FAMAS\u201903 (2003)"},{"key":"9080_CR38","first-page":"1167","volume-title":"Proceedings of the First International Joint Conference on Autonomous Agents and Multi-Agent Systems (AAMAS-02)","author":"W. Hoek van der","year":"2002","unstructured":"van der Hoek, W., Wooldridge, M.: Tractable multiagent planning for epistemic goals. In: Castelfranchi, C., Johnson, W.L. (eds.) Proceedings of the First International Joint Conference on Autonomous Agents and Multi-Agent Systems (AAMAS-02), pp.\u00a01167\u20131174. ACM Press, New York (2002)"},{"issue":"1","key":"9080_CR39","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1023\/A:1026185103185","volume":"75","author":"W. Hoek van der","year":"2003","unstructured":"van der Hoek, W., Wooldridge, M.: Cooperation, knowledge and time: alternating-time temporal epistemic logic and its applications. Stud. Log. 75(1), 125\u2013157 (2003)","journal-title":"Stud. Log."},{"key":"9080_CR40","doi-asserted-by":"crossref","unstructured":"van der Hoek, W., Lomuscio, A., Wooldridge, M.: On the complexity of practical ATL model checking. In: Stone, P., Weiss, G. (eds.) Proceedings of AAMAS\u201906, pp.\u00a0201\u2013208 (2006)","DOI":"10.1145\/1160633.1160665"},{"key":"9080_CR41","first-page":"35","volume":"XX","author":"S. Otterloo van","year":"2004","unstructured":"van Otterloo, S., Jonker, G.: On epistemic temporal strategic logic. Electron. Notes Theor. Comput. Sci. XX, 35\u201345 (2004). Proceedings of LCMAS\u201904","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"9080_CR42","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/5804.001.0001","volume-title":"Reasoning about Rational Agents","author":"M. Wooldridge","year":"2000","unstructured":"Wooldridge, M.: Reasoning about Rational Agents. MIT Press, Cambridge (2000)"}],"container-title":["Theory of Computing Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00224-007-9080-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00224-007-9080-z\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00224-007-9080-z","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,22]],"date-time":"2025-01-22T00:22:46Z","timestamp":1737505366000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s00224-007-9080-z"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007,10,30]]},"references-count":42,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2008,4]]}},"alternative-id":["9080"],"URL":"https:\/\/doi.org\/10.1007\/s00224-007-9080-z","relation":{},"ISSN":["1432-4350","1433-0490"],"issn-type":[{"type":"print","value":"1432-4350"},{"type":"electronic","value":"1433-0490"}],"subject":[],"published":{"date-parts":[[2007,10,30]]}}}