{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,12]],"date-time":"2025-02-12T05:27:58Z","timestamp":1739338078972,"version":"3.37.0"},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642027338"},{"type":"electronic","value":"9783642027345"}],"license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"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":[[2009]]},"DOI":"10.1007\/978-3-642-02734-5_1","type":"book-chapter","created":{"date-parts":[[2009,8,1]],"date-time":"2009-08-01T12:43:31Z","timestamp":1249130611000},"page":"1-12","source":"Crossref","is-referenced-by-count":4,"title":["Easy Yet Hard: Model Checking Strategies of Agents"],"prefix":"10.1007","author":[{"given":"Wojciech","family":"Jamroga","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"1","key":"1_CR1","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1023\/A:1008739929481","volume":"15","author":"R. Alur","year":"1999","unstructured":"Alur, R., Henzinger, T.A.: Reactive modules. Formal Methods in System Design\u00a015(1), 7\u201348 (1999)","journal-title":"Formal Methods in System Design"},{"key":"1_CR2","doi-asserted-by":"publisher","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. 100\u2013109. IEEE Computer Society Press, Los Alamitos (1997)"},{"key":"1_CR3","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"},{"key":"1_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/BFb0025774","volume-title":"Proceedings of Logics of Programs Workshop","author":"E.M. Clarke","year":"1981","unstructured":"Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching time temporal logic. In: Proceedings of Logics of Programs Workshop. LNCS, vol.\u00a0131, pp. 52\u201371. Springer, Heidelberg (1981)"},{"issue":"2","key":"1_CR5","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"},{"issue":"1","key":"1_CR6","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 \u201cnot 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":"1_CR7","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/5803.001.0001","volume-title":"Reasoning about Knowledge","author":"R. Fagin","year":"1995","unstructured":"Fagin, R., Halpern, J.Y., Moses, Y., Vardi, M.Y.: Reasoning about Knowledge. MIT Press, Cambridge (1995)"},{"key":"1_CR8","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"},{"key":"1_CR9","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":"1_CR10","series-title":"Lecture Notes in Computer Science","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, vol.\u00a03690, pp. 398\u2013407. Springer, Heidelberg (2005)"},{"issue":"3","key":"1_CR11","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","key":"1_CR12","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"},{"issue":"6","key":"1_CR13","doi-asserted-by":"publisher","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. Information Processing Letters\u00a054(6), 343\u2013345 (1995)","journal-title":"Information Processing Letters"},{"key":"1_CR14","unstructured":"Laroussinie, F., Markey, N., Oreiby, G.: Expressiveness and complexity of ATL. Technical Report LSV-06-03, CNRS & ENS Cachan, France (2006)"},{"key":"1_CR15","doi-asserted-by":"publisher","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 Publishers, Dordrecht (1993)"},{"key":"1_CR16","unstructured":"Raimondi, F.: Model Checking Multi-Agent Systems. PhD thesis, University College London (2006)"},{"key":"1_CR17","doi-asserted-by":"crossref","unstructured":"Schobbens, P.Y.: Alternating-time logic with imperfect recall. Electronic Notes in Theoretical Computer Science\u00a085(2) (2004)","DOI":"10.1016\/S1571-0661(05)82604-0"},{"key":"1_CR18","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"}],"container-title":["Lecture Notes in Computer Science","Computational Logic in Multi-Agent Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-02734-5_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,11]],"date-time":"2025-02-11T16:08:36Z","timestamp":1739290116000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-02734-5_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642027338","9783642027345"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-02734-5_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}