{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,4,3]],"date-time":"2025-04-03T04:10:26Z","timestamp":1743653426399,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":105,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642314841"},{"type":"electronic","value":"9783642314858"}],"license":[{"start":{"date-parts":[[2012,1,1]],"date-time":"2012-01-01T00:00:00Z","timestamp":1325376000000},"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":[[2012]]},"DOI":"10.1007\/978-3-642-31485-8_6","type":"book-chapter","created":{"date-parts":[[2012,6,22]],"date-time":"2012-06-22T19:13:03Z","timestamp":1340392383000},"page":"210-263","source":"Crossref","is-referenced-by-count":3,"title":["Specification and Verification of Multi-Agent Systems"],"prefix":"10.1007","author":[{"given":"Wojciech","family":"Jamroga","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Wojciech","family":"Penczek","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"2","key":"6_CR1","doi-asserted-by":"publisher","first-page":"377","DOI":"10.1007\/s11229-005-3875-8","volume":"149","author":"T. \u00c5gotnes","year":"2006","unstructured":"\u00c5gotnes, T.: Action and knowledge in alternating-time temporal logic. Synthese\u00a0149(2), 377\u2013409 (2006); Section on Knowledge, Rationality and Action","journal-title":"Synthese"},{"key":"6_CR2","doi-asserted-by":"crossref","unstructured":"\u00c5gotnes, T., Goranko, V., Jamroga, W.: Alternating-time temporal logics with irrevocable strategies. In: Samet, D. (ed.) Proceedings of TARK XI, pp. 15\u201324 (2007)","DOI":"10.1145\/1324249.1324256"},{"key":"6_CR3","doi-asserted-by":"crossref","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. 100\u2013109. IEEE Computer Society Press (1997)","DOI":"10.1109\/SFCS.1997.646098"},{"key":"6_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.A., Kupferman, O.: Alternating-time Temporal Logic. Journal of the ACM\u00a049, 672\u2013713 (2002)","journal-title":"Journal of the ACM"},{"issue":"3","key":"6_CR5","doi-asserted-by":"publisher","first-page":"241","DOI":"10.1145\/320613.320614","volume":"5","author":"C. Beeri","year":"1980","unstructured":"Beeri, C.: On the membership problem for functional and multivalued dependencies in relational databases. ACM Transactions on Database Systems\u00a05(3), 241\u2013259 (1980)","journal-title":"ACM Transactions on Database Systems"},{"key":"6_CR6","doi-asserted-by":"crossref","unstructured":"Biere, A., Cimatti, A., Clarke, E., Strichman, O., Zhu, Y.: Bounded model checking. In: Highly Dependable Software. Advances in Computers, vol.\u00a058. Academic Press (2003) (pre-print)","DOI":"10.1016\/S0065-2458(03)58003-2"},{"key":"6_CR7","doi-asserted-by":"crossref","unstructured":"Blackburn, P., de Rijke, M., Venema, Y.: Modal Logic. Cambridge Tracts in Theoretical Computer Science, vol.\u00a053. Cambridge University Press (2001)","DOI":"10.1017\/CBO9781107050884"},{"key":"6_CR8","unstructured":"Bulling, N.: Model checking coalition logic on implicit models is \u03943-complete. Technical Report IfI-10-02, Clausthal University of Technology (2010)"},{"key":"6_CR9","doi-asserted-by":"crossref","unstructured":"Bulling, N., Dix, J., Jamroga, W.: Model checking logics of strategic ability: Complexity. In: Dastani, M., Hindriks, K., Meyer, J.-J. (eds.) Specification and Verification of Multi-Agent Systems, pp. 125\u2013159. Springer (2010)","DOI":"10.1007\/978-1-4419-6984-2_5"},{"issue":"1-3","key":"6_CR10","doi-asserted-by":"crossref","first-page":"81","DOI":"10.3233\/FI-2009-0089","volume":"93","author":"N. Bulling","year":"2009","unstructured":"Bulling, N., Jamroga, W.: What agents can probably enforce. Fundamenta Informaticae\u00a093(1-3), 81\u201396 (2009)","journal-title":"Fundamenta Informaticae"},{"key":"6_CR11","unstructured":"Bulling, N., Jamroga, W.: Alternating epistemic mu-calculus. In: Proceedings of IJCAI 2011, pp. 109\u2013114 (2011)"},{"issue":"1-4","key":"6_CR12","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1007\/s10472-009-9110-4","volume":"53","author":"N. Bulling","year":"2008","unstructured":"Bulling, N., Jamroga, W., Dix, J.: Reasoning about temporal properties of rational play. Annals of Mathematics and Artificial Intelligence\u00a053(1-4), 51\u2013114 (2008)","journal-title":"Annals of Mathematics and Artificial Intelligence"},{"issue":"2","key":"6_CR13","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"E. Clarke","year":"1986","unstructured":"Clarke, E., Emerson, E.A., Sistla, A.P.: Automatic verification of finite state concurrent systems using temporal logic specifications: A practical approach. ACM Transactions on Programming Languages and Systems\u00a08(2), 244\u2013263 (1986)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"issue":"2","key":"6_CR14","doi-asserted-by":"publisher","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 Transactions on Programming Languages and Systems\u00a08(2), 244\u2013263 (1986)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"6_CR15","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press (1999)"},{"key":"6_CR16","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1016\/0004-3702(90)90055-5","volume":"42","author":"P.R. Cohen","year":"1990","unstructured":"Cohen, P.R., Levesque, H.J.: Intention is choice with commitment. Artificial Intelligence\u00a042, 213\u2013261 (1990)","journal-title":"Artificial Intelligence"},{"issue":"7","key":"6_CR17","doi-asserted-by":"publisher","first-page":"394","DOI":"10.1145\/368273.368557","volume":"5","author":"M. Davis","year":"1962","unstructured":"Davis, M., Logemann, G., Loveland, D.: A machine program for theorem proving. Journal of the ACM\u00a05(7), 394\u2013397 (1962)","journal-title":"Journal of the ACM"},{"issue":"3","key":"6_CR18","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1145\/321033.321034","volume":"7","author":"M. Davis","year":"1960","unstructured":"Davis, M., Putnam, H.: A computing procedure for quantification theory. Journal of the ACM\u00a07(3), 201\u2013215 (1960)","journal-title":"Journal of the ACM"},{"key":"6_CR19","doi-asserted-by":"publisher","first-page":"139","DOI":"10.1016\/j.tcs.2005.07.033","volume":"345","author":"L. Alfaro de","year":"2005","unstructured":"de Alfaro, L., Faella, M., Henzinger, T.A., Majumdar, R., Stoelinga, M.: Model checking discounted temporal properties. Theoretical Computer Science\u00a0345, 139\u2013170 (2005)","journal-title":"Theoretical Computer Science"},{"key":"6_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"278","DOI":"10.1007\/3-540-36577-X_20","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"P. Dembinski","year":"2003","unstructured":"Dembinski, P., Janowska, A., Janowski, P., Penczek, W., P\u00f3\u0142rola, A., Szreter, M., Wo\u017ana, B., Zbrzezny, A.: $\\surd$ erics: A Tool for Verifying Timed Automata and Estelle Specifications. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol.\u00a02619, pp. 278\u2013283. Springer, Heidelberg (2003)"},{"key":"6_CR21","unstructured":"Dima, C., Tiplea, F.L.: Model-checking atl under imperfect information and perfect recall semantics is undecidable. CoRR, abs\/1102.4225 (2011)"},{"key":"6_CR22","doi-asserted-by":"crossref","unstructured":"Doyen, L., Raskin, J.-F.: Games with imperfect information: Theory and algorithms. Lecture Notes in Game Theory for Computer Scientists, pp. 185\u2013212. Cambridge University Press (2011)","DOI":"10.1017\/CBO9780511973468.007"},{"key":"6_CR23","doi-asserted-by":"crossref","unstructured":"Emerson, E.A.: Temporal and modal logic. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, vol.\u00a0B, pp. 995\u20131072. Elsevier Science Publishers (1990)","DOI":"10.1016\/B978-0-444-88074-1.50021-4"},{"key":"6_CR24","unstructured":"Emerson, E.A., Lei, C.-L.: Efficient model checking in fragments of the propositional mu-calculus. In: Proc. of the 1st Symp. on Logic in Computer Science (LICS 1986), pp. 267\u2013278. IEEE Computer Society (1986)"},{"issue":"3","key":"6_CR25","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1016\/0167-6423(87)90036-0","volume":"8","author":"E.A. Emerson","year":"1987","unstructured":"Emerson, E.A., Lei, C.-L.: Modalities for model checking: Branching time logic strikes back. Science of Computer Programming\u00a08(3), 275\u2013306 (1987)","journal-title":"Science of Computer Programming"},{"key":"6_CR26","doi-asserted-by":"publisher","first-page":"14","DOI":"10.1145\/800057.808661","volume-title":"STOC 1984: Proceedings of the Sixteenth Annual ACM Symposium on Theory of Computing","author":"E.A. Emerson","year":"1984","unstructured":"Emerson, E.A., Sistla, A.P.: Deciding branching time logic. In: STOC 1984: Proceedings of the Sixteenth Annual ACM Symposium on Theory of Computing, pp. 14\u201324. ACM, New York (1984)"},{"issue":"1","key":"6_CR27","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1145\/4904.4999","volume":"33","author":"E.A. Emerson","year":"1986","unstructured":"Emerson, E.A., Halpern, J.Y.: \u201csometimes\u201d and \u201dnot never\u201d revisited: On branching versus linear time temporal logic. Journal of the ACM\u00a033(1), 151\u2013178 (1986)","journal-title":"Journal of the ACM"},{"key":"6_CR28","doi-asserted-by":"crossref","unstructured":"Fagin, R., Halpern, J.Y., Moses, Y., Vardi, M.Y.: Reasoning about Knowledge. MIT Press (1995)","DOI":"10.7551\/mitpress\/5803.001.0001"},{"key":"6_CR29","unstructured":"Fisher, M.: Temporal Logics. Kluwer (2006)"},{"key":"6_CR30","doi-asserted-by":"crossref","unstructured":"Fitting, M.: First-Order Logic and Automated Theorem Proving. Springer (1990)","DOI":"10.1007\/978-1-4684-0357-2"},{"key":"6_CR31","doi-asserted-by":"publisher","first-page":"13","DOI":"10.1007\/BF01744431","volume":"17","author":"M. Furst","year":"1984","unstructured":"Furst, M., Saxe, J.B., Sipser, M.: Parity, circuits, and the polynomial-time hierarchy. Math. Systems Theory\u00a017, 13\u201327 (1984)","journal-title":"Math. Systems Theory"},{"key":"6_CR32","unstructured":"Goranko, V., Jamroga, W.: State and path effectivity models for logics of multi-player games. In: Proceedings of AAMAS (to appear, 2012)"},{"key":"6_CR33","unstructured":"Goranko, V., Jamroga, W., Turrini, P.: Strategic games and truly playable effectivity functions. In: Proceedings of AAMAS 2011, pp. 727\u2013734 (2011)"},{"issue":"1","key":"6_CR34","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1016\/j.tcs.2005.07.043","volume":"353","author":"V. Goranko","year":"2006","unstructured":"Goranko, V., van Drimmelen, G.: Complete axiomatization and decidability of alternating-time temporal logic. Theoretical Computer Science\u00a0353(1), 93\u2013117 (2006)","journal-title":"Theoretical Computer Science"},{"issue":"1","key":"6_CR35","doi-asserted-by":"publisher","first-page":"93","DOI":"10.3166\/jancl.21.93-131","volume":"21","author":"D.P. Guelev","year":"2011","unstructured":"Guelev, D.P., Dima, C., Enea, C.: An alternating-time temporal logic with knowledge, perfect recall and past: axiomatisation and model-checking. Journal of Applied Non-Classical Logics\u00a021(1), 93\u2013131 (2011)","journal-title":"Journal of Applied Non-Classical Logics"},{"key":"6_CR36","doi-asserted-by":"crossref","unstructured":"Halpern, J.Y.: Reasoning about knowledge: a survey. In: Gabbay, D.M., Hogger, C.J., Robinson, J.A. (eds.) The Handbook of Logic in Artificial Intelligence and Logic Programming, vol.\u00a0IV, pp. 1\u201334. Oxford University Press (1995)","DOI":"10.1093\/oso\/9780198534532.003.0001"},{"key":"6_CR37","doi-asserted-by":"crossref","unstructured":"Harel, D., Kozen, D., Tiuryn, J.: Dynamic Logic. MIT Press (2000)","DOI":"10.7551\/mitpress\/2516.001.0001"},{"issue":"2-4","key":"6_CR38","first-page":"281","volume":"57","author":"B.P. Harrenstein","year":"2003","unstructured":"Harrenstein, B.P., van der Hoek, W., Meyer, J.-J., Witteveen, C.: A modal characterization of Nash equilibrium. Fundamenta Informaticae\u00a057(2-4), 281\u2013321 (2003)","journal-title":"Fundamenta Informaticae"},{"key":"6_CR39","unstructured":"Harrenstein, P., van der Hoek, W., Meijer, J.-J., Witteveen, C.: Subgame-perfect Nash equilibria in dynamic logic. In: Pauly, M., Baltag, A. (eds.) Proceedings of the ILLC Workshop on Logic and Games, vol.\u00a025, pp. 29\u201330. University of Amsterdam (2002); Tech. Report PP-1999-25"},{"key":"6_CR40","unstructured":"Hawke, P.: Coordination, almost perfect information and strategic ability. In: Proceedings of LAMAS (2010)"},{"key":"6_CR41","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1007\/3-540-46017-9_9","volume-title":"Model Checking Software","author":"W. Hoek van der","year":"2002","unstructured":"van der Hoek, W., Wooldridge, M.: Model Checking Knowledge and Time. In: Bo\u0161na\u010dki, D., Leue, S. (eds.) SPIN 2002. LNCS, vol.\u00a02318, pp. 95\u2013111. Springer, Heidelberg (2002)"},{"key":"6_CR42","unstructured":"Huang, X., Su, K., Zhang, C.: Probabilistic alternating-time temporal logic of incomplete information and synchronous perfect recall. In: Proceedings of AAAI 2012 (to appear, 2012)"},{"key":"6_CR43","doi-asserted-by":"crossref","unstructured":"Huth, M., Ryan, M.: Logic in Computer Science: Modelling and Reasoning about Systems. Cambridge University Press (2004)","DOI":"10.1017\/CBO9780511810275"},{"issue":"3","key":"6_CR44","doi-asserted-by":"publisher","first-page":"384","DOI":"10.1016\/0022-0000(81)90039-8","volume":"22","author":"N. Immerman","year":"1981","unstructured":"Immerman, N.: Number of quantifiers is better than number of tape cells. Journal of Computer and System Sciences\u00a022(3), 384\u2013406 (1981)","journal-title":"Journal of Computer and System Sciences"},{"key":"6_CR45","unstructured":"Jamroga, W.: Some remarks on alternating temporal epistemic logic. In: Dunin-Keplicz, B., Verbrugge, R. (eds.) Proceedings of Formal Approaches to Multi-Agent Systems (FAMAS 2003), pp. 133\u2013140 (2003)"},{"key":"6_CR46","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"239","DOI":"10.1007\/978-3-540-89674-6_27","volume-title":"Intelligent Agents and Multi-Agent Systems","author":"W. Jamroga","year":"2008","unstructured":"Jamroga, W.: A Temporal Logic for Stochastic Multi-Agent Systems. In: Bui, T.D., Ho, T.V., Ha, Q.T. (eds.) PRIMA 2008. LNCS (LNAI), vol.\u00a05357, pp. 239\u2013250. Springer, Heidelberg (2008)"},{"key":"6_CR47","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-02734-5_1","volume-title":"Computational Logic in Multi-Agent Systems","author":"W. Jamroga","year":"2009","unstructured":"Jamroga, W.: Easy Yet Hard: Model Checking Strategies of Agents. In: Fisher, M., Sadri, F., Thielscher, M. (eds.) CLIMA IX. LNCS, vol.\u00a05405, pp. 1\u201312. Springer, Heidelberg (2009)"},{"key":"6_CR48","doi-asserted-by":"crossref","unstructured":"Jamroga, W., \u00c5gotnes, T.: Modular interpreted systems: A preliminary report. Technical Report IfI-06-15, Clausthal University of Technology (2006)","DOI":"10.1145\/1329125.1329286"},{"issue":"4","key":"6_CR49","doi-asserted-by":"publisher","first-page":"423","DOI":"10.3166\/jancl.17.423-475","volume":"17","author":"W. Jamroga","year":"2007","unstructured":"Jamroga, W., \u00c5gotnes, T.: Constructive knowledge: What agents can achieve under incomplete information. Journal of Applied Non-Classical Logics\u00a017(4), 423\u2013475 (2007)","journal-title":"Journal of Applied Non-Classical Logics"},{"key":"6_CR50","doi-asserted-by":"crossref","unstructured":"Jamroga, W., \u00c5gotnes, T.: Modular interpreted systems. In: Proceedings of AAMAS 2007, pp. 892\u2013899 (2007)","DOI":"10.1145\/1329125.1329286"},{"key":"6_CR51","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"398","DOI":"10.1007\/11559221_40","volume-title":"Multi-Agent Systems and Applications IV","author":"W. Jamroga","year":"2005","unstructured":"Jamroga, W., Dix, J.: Do Agents Make Model Checking Explode (Computationally)? In: P\u011bchou\u010dek, M., Petta, P., Varga, L.Z. (eds.) CEEMAS 2005. LNCS (LNAI), vol.\u00a03690, pp. 398\u2013407. Springer, Heidelberg (2005)"},{"key":"6_CR52","unstructured":"Jamroga, W., Dix, J.: Model checking ATL ir is indeed $\\Delta_2^P$ -complete. In: Proceedings of EUMAS 2006 (2006)"},{"issue":"3","key":"6_CR53","doi-asserted-by":"publisher","first-page":"366","DOI":"10.1007\/s00224-007-9080-z","volume":"42","author":"W. Jamroga","year":"2008","unstructured":"Jamroga, W., Dix, J.: Model checking abilities of agents: A closer look. Theory of Computing Systems\u00a042(3), 366\u2013410 (2008)","journal-title":"Theory of Computing Systems"},{"issue":"2-3","key":"6_CR54","first-page":"185","volume":"63","author":"W. Jamroga","year":"2004","unstructured":"Jamroga, W., van der Hoek, W.: Agents that know how to play. Fundamenta Informaticae\u00a063(2-3), 185\u2013219 (2004)","journal-title":"Fundamenta Informaticae"},{"key":"6_CR55","unstructured":"Jonker, G.: Feasible strategies in Alternating-time Temporal Epistemic Logic. Master thesis, University of Utrecht (2003)"},{"key":"6_CR56","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"189","DOI":"10.1007\/978-3-540-30960-4_13","volume-title":"Formal Approaches to Agent-Based Systems","author":"M. Kacprzak","year":"2004","unstructured":"Kacprzak, M., Lomuscio, A., \u0141asica, T., Penczek, W., Szreter, M.: Verifying Multi-agent Systems via Unbounded Model Checking. In: Hinchey, M.G., Rash, J.L., Truszkowski, W.F., Rouff, C.A. (eds.) FAABS 2004. LNCS (LNAI), vol.\u00a03228, pp. 189\u2013212. Springer, Heidelberg (2004)"},{"issue":"1-2","key":"6_CR57","first-page":"215","volume":"72","author":"M. Kacprzak","year":"2006","unstructured":"Kacprzak, M., Lomuscio, A., Niewiadomski, A., Penczek, W., Raimondi, F., Szreter, M.: Comparing BDD and SAT based techniques for model checking Chaum\u2019s dining cryptographers protocol. Fundamenta Informaticae\u00a072(1-2), 215\u2013234 (2006)","journal-title":"Fundamenta Informaticae"},{"issue":"2-3","key":"6_CR58","first-page":"221","volume":"63","author":"M. Kacprzak","year":"2004","unstructured":"Kacprzak, M., Lomuscio, A., Penczek, W.: From bounded to unbounded model checking for temporal epistemic logic. Fundamenta Informaticae\u00a063(2-3), 221\u2013240 (2004)","journal-title":"Fundamenta Informaticae"},{"issue":"2-3","key":"6_CR59","first-page":"221","volume":"63","author":"M. Kacprzak","year":"2004","unstructured":"Kacprzak, M., Lomuscio, A., Penczek, W.: From bounded to unbounded model checking for temporal epistemic logic. Fundam. Inform.\u00a063(2-3), 221\u2013240 (2004)","journal-title":"Fundam. Inform."},{"issue":"1-4","key":"6_CR60","first-page":"313","volume":"85","author":"M. Kacprzak","year":"2008","unstructured":"Kacprzak, M., Nabialek, W., Niewiadomski, A., Penczek, W., P\u00f3lrola, A., Szreter, M., Wo\u017ana, B., Zbrzezny, A.: VerICS 2007 - a model checker for knowledge and real-time. Fundamenta Informaticae\u00a085(1-4), 313\u2013328 (2008)","journal-title":"Fundamenta Informaticae"},{"issue":"1","key":"6_CR61","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1007\/s10458-005-0944-9","volume":"11","author":"M. Kacprzak","year":"2005","unstructured":"Kacprzak, M., Penczek, W.: Fully symbolic unbounded model checking for alternating-time temporal logic. Autonomous Agents and Multi-Agent Systems\u00a011(1), 69\u201389 (2005)","journal-title":"Autonomous Agents and Multi-Agent Systems"},{"key":"6_CR62","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1016\/0304-3975(82)90125-6","volume":"27","author":"D. Kozen","year":"1983","unstructured":"Kozen, D.: Results on the propositional mu-calculus. Theoretical Computer Science\u00a027, 333\u2013354 (1983)","journal-title":"Theoretical Computer Science"},{"issue":"2","key":"6_CR63","doi-asserted-by":"publisher","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. Journal of the ACM\u00a047(2), 312\u2013360 (2000)","journal-title":"Journal of the ACM"},{"key":"6_CR64","doi-asserted-by":"publisher","first-page":"7","DOI":"10.2168\/LMCS-4(2:7)2008","volume":"4","author":"F. Laroussinie","year":"2008","unstructured":"Laroussinie, F., Markey, N., Oreiby, G.: On the expressiveness and complexity of ATL. Logical Methods in Computer Science\u00a04, 7 (2008)","journal-title":"Logical Methods in Computer Science"},{"key":"6_CR65","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"318","DOI":"10.1007\/3-540-45315-6_21","volume-title":"Foundations of Software Science and Computation Structures","author":"F. Laroussinie","year":"2001","unstructured":"Laroussinie, F., Markey, N., Schnoebelen, P.: Model Checking CTL\u2009+\u2009 and FCTL is Hard. In: Honsell, F., Miculan, M. (eds.) FOSSACS 2001. LNCS, vol.\u00a02030, pp. 318\u2013331. Springer, Heidelberg (2001)"},{"key":"6_CR66","doi-asserted-by":"crossref","unstructured":"Leyton-Brown, K., Shoham, Y.: Essentials of Game Theory: A Concise, Multidisciplinary Introduction. Morgan & Claypool (2008)","DOI":"10.2200\/S00108ED1V01Y200802AIM003"},{"key":"6_CR67","first-page":"97","volume-title":"POPL 1985: Proceedings of the 12th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages","author":"O. Lichtenstein","year":"1985","unstructured":"Lichtenstein, O., Pnueli, A.: Checking that finite state concurrent programs satisfy their linear specification. In: POPL 1985: Proceedings of the 12th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, pp. 97\u2013107. ACM, New York (1985)"},{"key":"6_CR68","doi-asserted-by":"crossref","unstructured":"Lomuscio, A., Penczek, W.: Logic column 19: Symbolic model checking for temporal-epistemic logics. CoRR, abs\/0709.0446 (2007)","DOI":"10.1145\/1324215.1324231"},{"key":"6_CR69","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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.\u00a05643, pp. 682\u2013688. Springer, Heidelberg (2009)"},{"key":"6_CR70","doi-asserted-by":"crossref","unstructured":"Moskewicz, M., Madigan, C., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an efficient SAT solver. In: Proc. of the 38th Design Automation Conference (DAC 2001), pp. 530\u2013535 (June 2001)","DOI":"10.1145\/378239.379017"},{"key":"6_CR71","unstructured":"Osborne, M., Rubinstein, A.: A Course in Game Theory. MIT Press (1994)"},{"key":"6_CR72","volume-title":"Computational Complexity","author":"C.H. Papadimitriou","year":"1994","unstructured":"Papadimitriou, C.H.: Computational Complexity. Addison Wesley, Reading (1994)"},{"key":"6_CR73","unstructured":"Pauly, M.: Logic for Social Software. PhD thesis, University of Amsterdam (2001)"},{"key":"6_CR74","doi-asserted-by":"crossref","unstructured":"Penczek, W., Lomuscio, A.: Verifying epistemic properties of multi-agent systems via bounded model checking. In: Proc. of the 2nd Int. Conf. on Autonomous Agents and Multi-Agent Systems (AAMAS 2003), pp. 209\u2013216. ACM (2003)","DOI":"10.1145\/860575.860609"},{"issue":"2","key":"6_CR75","first-page":"167","volume":"55","author":"W. Penczek","year":"2003","unstructured":"Penczek, W., Lomuscio, A.: Verifying epistemic properties of multi-agent systems via bounded model checking. Fundamenta Informaticae\u00a055(2), 167\u2013185 (2003)","journal-title":"Fundamenta Informaticae"},{"key":"6_CR76","doi-asserted-by":"crossref","unstructured":"Penczek, W., Polrola, A.: Advances in Verification of Time Petri Nets and Timed Automata: A Temporal Logic Approach. SCI, vol.\u00a020. Springer (2006)","DOI":"10.1007\/978-3-540-32870-4"},{"key":"6_CR77","doi-asserted-by":"crossref","unstructured":"Peterson, G., Reif, J.: Multiple-person alternation. In: Proceedings of the 20th Annual Symposium on Foundations of Computer Science (FOCS), pp. 348\u2013363. IEEE Computer Society Press (1979)","DOI":"10.1109\/SFCS.1979.25"},{"key":"6_CR78","doi-asserted-by":"crossref","unstructured":"Peterson, G., Reif, J., Azhar, S.: Lower bounds for multiplayer noncooperative games of incomplete information. Computers and Mathematics with Applications 41(7), 957\u2013992","DOI":"10.1016\/S0898-1221(00)00333-3"},{"key":"6_CR79","first-page":"179","volume-title":"POPL 1989: Proceedings of the 16th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","author":"A. Pnueli","year":"1989","unstructured":"Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: POPL 1989: Proceedings of the 16th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 179\u2013190. ACM, New York (1989)"},{"key":"6_CR80","doi-asserted-by":"crossref","unstructured":"Pnueli, A., Rosner, R.: Distributed reactive systems are hard to synthesize. In: Proceedings of the 31th Annual Symposium on Foundations of Computer Science (FOCS), pp. 746\u2013757. IEEE Computer Society Press (1990)","DOI":"10.1109\/FSCS.1990.89597"},{"key":"6_CR81","unstructured":"Raimondi, F.: Model Checking Multi-Agent Systems. PhD thesis, University College London (2006)"},{"key":"6_CR82","doi-asserted-by":"crossref","unstructured":"Raimondi, F., Lomuscio, A.: Automatic verification of deontic interpreted systems by model checking via OBDD\u2019s. In: de M\u00e1ntaras, R.L., Saitta, L. (eds.) Proceedings of ECAI, pp. 53\u201357 (2004)","DOI":"10.1007\/978-3-540-25927-5_15"},{"key":"6_CR83","unstructured":"Raimondi, F., Lomuscio, A.: Verification of multiagent systems via ordered binary decision diagrams: An algorithm and its implementation. In: AAMAS, pp. 630\u2013637 (2004)"},{"key":"6_CR84","unstructured":"Rao, A.S., Georgeff, M.P.: Modeling rational agents within a BDI-architecture. In: Proceedings of the 2nd International Conference on Principles of Knowledge Representation and Reasoning, pp. 473\u2013484 (1991)"},{"key":"6_CR85","unstructured":"Rosner, R.: Modular Synthesis of Reactive Systems. PhD thesis, Weizmann Institute of Science (1992)"},{"key":"6_CR86","unstructured":"Schnoebelen, P.: The complexity of temporal model checking. In: Advances in Modal Logics, Proceedings of AiML 2002. World Scientific (2003)"},{"key":"6_CR87","unstructured":"Schnoor, H.: Strategic planning for probabilistic games with incomplete information. In: Proceedings of AAMAS 2010, pp. 1057\u20131064 (2010)"},{"issue":"2","key":"6_CR88","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1016\/S1571-0661(05)82604-0","volume":"85","author":"P.Y. Schobbens","year":"2004","unstructured":"Schobbens, P.Y.: Alternating-time logic with imperfect recall. Electronic Notes in Theoretical Computer Science\u00a085(2), 82\u201393 (2004)","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"6_CR89","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"108","DOI":"10.1007\/3-540-40922-X_8","volume-title":"Formal Methods in Computer-Aided Design","author":"M. Sheeran","year":"2000","unstructured":"Sheeran, M., Singh, S., St\u00e5lmarck, G.: Checking Safety Properties Using Induction and a SAT-Solver. In: Johnson, S.D., Hunt Jr., W.A. (eds.) FMCAD 2000. LNCS, vol.\u00a01954, pp. 108\u2013125. Springer, Heidelberg (2000)"},{"issue":"1-3","key":"6_CR90","first-page":"347","volume":"72","author":"N.V. Shilov","year":"2006","unstructured":"Shilov, N.V., Garanina, N.O., Choe, K.-M.: Update and abstraction in model checking of knowledge and branching time. Fundamenta Informaticae\u00a072(1-3), 347\u2013361 (2006)","journal-title":"Fundamenta Informaticae"},{"key":"6_CR91","unstructured":"Shilov, N.V., Garanina, N.O., Kalinina, N.A.: Model checking knowledge, actions and fixpoints. In: Proceedings of CS&P 2004, pp. 351\u2013357 (2004)"},{"issue":"3","key":"6_CR92","doi-asserted-by":"publisher","first-page":"733","DOI":"10.1145\/3828.3837","volume":"32","author":"A.P. Sistla","year":"1985","unstructured":"Sistla, A.P., Clarke, E.M.: The complexity of propositional linear temporal logics. Journal of ACM\u00a032(3), 733\u2013749 (1985)","journal-title":"Journal of ACM"},{"key":"6_CR93","doi-asserted-by":"crossref","unstructured":"Stirling, C.: Modal and Temporal Properties of Processes. Springer (2001)","DOI":"10.1007\/978-1-4757-3550-5"},{"key":"6_CR94","doi-asserted-by":"publisher","first-page":"285","DOI":"10.2140\/pjm.1955.5.285","volume":"5","author":"A. Tarski","year":"1955","unstructured":"Tarski, A.: A lattice-theoretical fixpoint theorem and its applications. Pacific Journal of Mathematics\u00a05, 285\u2013309 (1955)","journal-title":"Pacific Journal of Mathematics"},{"key":"6_CR95","doi-asserted-by":"crossref","unstructured":"van der Hoek, W., Jamroga, W., Wooldridge, M.: A logic for strategic reasoning. In: Proceedings of AAMAS 2005, pp. 157\u2013164 (2005)","DOI":"10.1145\/1082473.1082497"},{"key":"6_CR96","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 2006, pp. 201\u2013208 (2006)","DOI":"10.1145\/1160633.1160665"},{"key":"6_CR97","first-page":"53","volume":"8","author":"W. Hoek van der","year":"2002","unstructured":"van der Hoek, W., Verbrugge, R.: Epistemic logic: A survey. Game Theory and Applications\u00a08, 53\u201394 (2002)","journal-title":"Game Theory and Applications"},{"key":"6_CR98","doi-asserted-by":"publisher","first-page":"1167","DOI":"10.1145\/545056.545095","volume-title":"Proceedings of the First International Joint Conference on Autonomous Agents and Multi-Agent Systems (AAMAS 2002)","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 2002), pp. 1167\u20131174. ACM Press, New York (2002)"},{"issue":"1","key":"6_CR99","doi-asserted-by":"publisher","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. Studia Logica\u00a075(1), 125\u2013157 (2003)","journal-title":"Studia Logica"},{"key":"6_CR100","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"432","DOI":"10.1007\/3-540-46691-6_35","volume-title":"Foundations of Software Technology and Theoretical Computer Science","author":"R. Meyden van der","year":"1999","unstructured":"van der Meyden, R., Shilov, N.V.: Model Checking Knowledge and Time in Systems with Perfect Recall (Extended Abstract). In: Pandu Rangan, C., Raman, V., Sarukkai, S. (eds.) FST TCS 1999. LNCS, vol.\u00a01738, pp. 432\u2013445. Springer, Heidelberg (1999)"},{"key":"6_CR101","unstructured":"van Otterloo, S., Jonker, G.: On Epistemic Temporal Strategic Logic. Electronic Notes in Theoretical Computer Science XX, 35\u201345 (2004); Proceedings of LCMAS 2004"},{"key":"6_CR102","unstructured":"Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification (preliminary report). In: Proceedings of the First Annual IEEE Symposium on Logic in Computer Science (LICS 1986), pp. 332\u2013344. IEEE Computer Society Press (1986)"},{"key":"6_CR103","doi-asserted-by":"crossref","unstructured":"Walther, D., van der Hoek, W., Wooldridge, M.: Alternating-time temporal logic with explicit strategies. In: Samet, D. (ed.) Proceedings TARK XI, pp. 269\u2013278. Presses Universitaires de Louvain (2007)","DOI":"10.1145\/1324249.1324285"},{"volume-title":"Multiagent Systems. A Modern Approach to Distributed Artificial Intelligence","year":"1999","key":"6_CR104","unstructured":"Weiss, G. (ed.): Multiagent Systems. A Modern Approach to Distributed Artificial Intelligence. MIT Press, Cambridge (1999)"},{"key":"6_CR105","unstructured":"Wooldridge, M.: An Introduction to Multi Agent Systems. John Wiley & Sons (2002)"}],"container-title":["Lecture Notes in Computer Science","Lectures on Logic and Computation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-31485-8_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,2]],"date-time":"2025-04-02T11:49:17Z","timestamp":1743594557000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-31485-8_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642314841","9783642314858"],"references-count":105,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-31485-8_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}