{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,31]],"date-time":"2025-10-31T23:47:10Z","timestamp":1761954430081,"version":"build-2065373602"},"publisher-location":"Cham","reference-count":24,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032068460","type":"print"},{"value":"9783032068477","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,11,1]],"date-time":"2025-11-01T00:00:00Z","timestamp":1761955200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,11,1]],"date-time":"2025-11-01T00:00:00Z","timestamp":1761955200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"DOI":"10.1007\/978-3-032-06847-7_6","type":"book-chapter","created":{"date-parts":[[2025,10,31]],"date-time":"2025-10-31T23:42:25Z","timestamp":1761954145000},"page":"106-124","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Efficient Model Checking for\u00a0the\u00a0Alternating-Time $$\\mu $$-Calculus via\u00a0Effectivity Frames"],"prefix":"10.1007","author":[{"given":"Daniel","family":"Hausmann","sequence":"first","affiliation":[]},{"given":"Merlin","family":"Humml","sequence":"additional","affiliation":[]},{"given":"Simon","family":"Prucker","sequence":"additional","affiliation":[]},{"given":"Lutz","family":"Schr\u00f6der","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,11,1]]},"reference":[{"key":"6_CR1","doi-asserted-by":"publisher","unstructured":"Alur, R., et al.: JMOCHA: a model checking tool that exploits design structure. In: International Conference on Software Engineering, ICSE 2001, pp. 835\u2013836. IEEE Computer Society (2001). https:\/\/doi.org\/10.1109\/ICSE.2001.919196","DOI":"10.1109\/ICSE.2001.919196"},{"key":"6_CR2","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. J. ACM 49, 672\u2013713 (2002). https:\/\/doi.org\/10.1145\/585265.585270","journal-title":"J. ACM"},{"key":"6_CR3","doi-asserted-by":"publisher","unstructured":"Belardinelli, F., Jamroga, W., Kurpiewski, D., Malvone, V., Murano, A.: Strategy logic with simple goals: tractable reasoning about strategies. In: International Joint Conference on Artificial Intelligence, IJCAI 2019, pp. 88\u201394 (2019). https:\/\/doi.org\/10.24963\/IJCAI.2019\/13","DOI":"10.24963\/IJCAI.2019\/13"},{"key":"6_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"525","DOI":"10.1007\/978-3-319-08867-9_34","volume-title":"Computer Aided Verification","author":"P \u010cerm\u00e1k","year":"2014","unstructured":"\u010cerm\u00e1k, P., Lomuscio, A., Mogavero, F., Murano, A.: MCMAS-SLK: a model checker for the verification of strategy logic specifications. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 525\u2013532. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_34"},{"issue":"6","key":"6_CR5","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1016\/j.ic.2009.07.004","volume":"208","author":"K Chatterjee","year":"2010","unstructured":"Chatterjee, K., Henzinger, T.A., Piterman, N.: Strategy logic. Inf. Comput. 208(6), 677\u2013693 (2010). https:\/\/doi.org\/10.1016\/j.ic.2009.07.004","journal-title":"Inf. Comput."},{"key":"6_CR6","doi-asserted-by":"publisher","unstructured":"Goranko, V., Jamroga, W.: Comparing semantics of logics for multi-agent systems. In: Information, Interaction and Agency, pp. 77\u2013116 (2004). https:\/\/doi.org\/10.1007\/1-4020-4094-6_3","DOI":"10.1007\/1-4020-4094-6_3"},{"key":"6_CR7","doi-asserted-by":"publisher","unstructured":"Goranko, V., Kuusisto, A., R\u00f6nnholm, R.: Game-theoretic semantics for ATL$$ ^{\\text{+}}$$ with applications to model checking. Inf. Comput. 276, 104554 (2021). https:\/\/doi.org\/10.1016\/j.ic.2020.104554","DOI":"10.1016\/j.ic.2020.104554"},{"key":"6_CR8","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"396","DOI":"10.1007\/978-3-319-08587-6_31","volume-title":"Automated Reasoning","author":"D Gor\u00edn","year":"2014","unstructured":"Gor\u00edn, D., Pattinson, D., Schr\u00f6der, L., Widmann, F., Wi\u00dfmann, T.: Cool \u2013 a generic reasoner for coalgebraic hybrid logics (system description). In: Demri, S., Kapur, D., Weidenbach, C. (eds.) IJCAR 2014. LNCS (LNAI), vol. 8562, pp. 396\u2013402. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08587-6_31"},{"key":"6_CR9","doi-asserted-by":"publisher","unstructured":"G\u00f6rlitz, O., Hausmann, D., Humml, M., Pattinson, D., Prucker, S., Schr\u00f6der, L.: COOL 2 \u2013 a generic reasoner for modal fixpoint logics (system description). In: Automated Deduction, CADE 2023. LNCS, vol. 14132, pp. 234\u2013247. Springer, Heidelberg (2023). https:\/\/doi.org\/10.1007\/978-3-031-38499-8_14","DOI":"10.1007\/978-3-031-38499-8_14"},{"key":"6_CR10","doi-asserted-by":"publisher","unstructured":"Hausmann, D., Humml, M., Prucker, S., Schr\u00f6der, L., Strahlberger, A.: Generic model checking for modal fixpoint logics in COOL-MC. In: Verification, Model Checking, and Abstract Interpretation, VMCAI 2024. LNCS, vol. 14499, pp. 171\u2013185. Springer, Heidelberg (2024). https:\/\/doi.org\/10.1007\/978-3-031-50524-9_8","DOI":"10.1007\/978-3-031-50524-9_8"},{"key":"6_CR11","doi-asserted-by":"publisher","unstructured":"Hausmann, D., Schr\u00f6der, L.: Game-based local model checking for the coalgebraic $$\\mu $$-calculus. In: Concurrency Theory, CONCUR 2019. LIPIcs, vol.\u00a0140, pp. 35:1\u201335:16. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2019). https:\/\/doi.org\/10.4230\/LIPIcs.CONCUR.2019.35","DOI":"10.4230\/LIPIcs.CONCUR.2019.35"},{"key":"6_CR12","doi-asserted-by":"publisher","unstructured":"van\u00a0der Hoek, W., Lomuscio, A., Wooldridge, M.J.: On the complexity of practical ATL model checking. In: Autonomous Agents and Multiagent Systems, AAMAS 2006, pp. 201\u2013208. ACM (2006). https:\/\/doi.org\/10.1145\/1160633.1160665","DOI":"10.1145\/1160633.1160665"},{"key":"6_CR13","doi-asserted-by":"publisher","unstructured":"Ka\u0144ski, M., Niewiadomski, A., Kacprzak, M., Penczek, W., Nabia\u0142ek, W.: Unbounded model checking for ATL. Studia Informatica 25(1\u20132) (2021). https:\/\/doi.org\/10.34739\/si.2021.25.01","DOI":"10.34739\/si.2021.25.01"},{"key":"6_CR14","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. Theor. Comput. Sci. 27, 333\u2013354 (1983). https:\/\/doi.org\/10.1016\/0304-3975(82)90125-6","journal-title":"Theor. Comput. Sci."},{"key":"6_CR15","doi-asserted-by":"publisher","unstructured":"Kupke, C., Marti, J., Venema, Y.: Size measures and alphabetic equivalence in the $$\\mu $$-calculus. In: Logic in Computer Science, LICS 2022, pp. 18:1\u201318:13. ACM (2022). https:\/\/doi.org\/10.1145\/3531130.3533339","DOI":"10.1145\/3531130.3533339"},{"key":"6_CR16","doi-asserted-by":"publisher","unstructured":"Litak, T., Pattinson, D., Sano, K., Schr\u00f6der, L.: Model theory and proof theory of coalgebraic predicate logic. Log. Methods Comput. Sci. 14(1) (2018). https:\/\/doi.org\/10.23638\/LMCS-14(1:22)2018","DOI":"10.23638\/LMCS-14(1:22)2018"},{"issue":"1","key":"6_CR17","doi-asserted-by":"publisher","first-page":"9","DOI":"10.1007\/s10009-015-0378-x","volume":"19","author":"A Lomuscio","year":"2015","unstructured":"Lomuscio, A., Qu, H., Raimondi, F.: MCMAS: an open-source model checker for the verification of multi-agent systems. Int. J. Softw. Tools Technol. Transfer 19(1), 9\u201330 (2015). https:\/\/doi.org\/10.1007\/s10009-015-0378-x","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"key":"6_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"250","DOI":"10.1007\/3-540-45657-0_19","volume-title":"Computer Aided Verification","author":"KL McMillan","year":"2002","unstructured":"McMillan, K.L.: Applying SAT methods in unbounded symbolic model checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 250\u2013264. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45657-0_19"},{"key":"6_CR19","doi-asserted-by":"publisher","unstructured":"Mogavero, F., Murano, A., Perelli, G., Vardi, M.Y.: Reasoning about strategies: On the model-checking problem. ACM Trans. Comput. Log. 15(4), 34:1\u201334:47 (2014). https:\/\/doi.org\/10.1145\/2631917","DOI":"10.1145\/2631917"},{"issue":"1","key":"6_CR20","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1093\/logcom\/12.1.149","volume":"12","author":"M Pauly","year":"2002","unstructured":"Pauly, M.: A modal logic for coalitional power in games. J. Log. Comput. 12(1), 149\u2013166 (2002). https:\/\/doi.org\/10.1093\/logcom\/12.1.149","journal-title":"J. Log. Comput."},{"key":"6_CR21","unstructured":"Peter, D.: Hyperfine (2023). https:\/\/github.com\/sharkdp\/hyperfine"},{"issue":"7","key":"6_CR22","doi-asserted-by":"publisher","first-page":"1871","DOI":"10.1093\/logcom\/exw032","volume":"27","author":"J Pilecki","year":"2017","unstructured":"Pilecki, J., Bednarczyk, M.A., Jamroga, W.: SMC: synthesis of uniform strategies and verification of strategic ability for multi-agent systems. J. Log. Comput. 27(7), 1871\u20131895 (2017). https:\/\/doi.org\/10.1093\/logcom\/exw032","journal-title":"J. Log. Comput."},{"issue":"1","key":"6_CR23","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/S0304-3975(00)00056-6","volume":"249","author":"JJMM Rutten","year":"2000","unstructured":"Rutten, J.J.M.M.: Universal coalgebra: a theory of systems. Theor. Comput. Sci. 249(1), 3\u201380 (2000). https:\/\/doi.org\/10.1016\/S0304-3975(00)00056-6","journal-title":"Theor. Comput. Sci."},{"key":"6_CR24","unstructured":"tcsprojects: PGSolver. https:\/\/github.com\/tcsprojects\/pgsolver"}],"container-title":["Lecture Notes in Computer Science","Model Checking Software"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-06847-7_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,31]],"date-time":"2025-10-31T23:42:26Z","timestamp":1761954146000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-06847-7_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,11,1]]},"ISBN":["9783032068460","9783032068477"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-06847-7_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,11,1]]},"assertion":[{"value":"1 November 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"SPIN","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Model Checking Software","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Hamilton, ON","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Canada","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"7 May 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"8 May 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"31","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"spin2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/spin-web.github.io\/SPIN2024\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}