{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,10]],"date-time":"2026-02-10T20:27:14Z","timestamp":1770755234585,"version":"3.50.0"},"reference-count":74,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2026,2,9]],"date-time":"2026-02-09T00:00:00Z","timestamp":1770595200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by-nc-nd\/4.0"},{"start":{"date-parts":[[2026,2,9]],"date-time":"2026-02-09T00:00:00Z","timestamp":1770595200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by-nc-nd\/4.0"}],"funder":[{"name":"National Centre for Research and Development (Poland) & National Research Fund","award":["POLLUX-XI\/14\/SpaceVote\/2023"],"award-info":[{"award-number":["POLLUX-XI\/14\/SpaceVote\/2023"]}]},{"DOI":"10.13039\/501100014434","name":"Narodowa Agencja Wymiany Akademickiej","doi-asserted-by":"publisher","award":["BPN\/BFR\/2023\/1\/00045"],"award-info":[{"award-number":["BPN\/BFR\/2023\/1\/00045"]}],"id":[{"id":"10.13039\/501100014434","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Auton Agent Multi-Agent Syst"],"published-print":{"date-parts":[[2026,6]]},"DOI":"10.1007\/s10458-025-09726-4","type":"journal-article","created":{"date-parts":[[2026,2,9]],"date-time":"2026-02-09T10:35:24Z","timestamp":1770633324000},"update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Strategic (timed) computation tree logic"],"prefix":"10.1007","volume":"40","author":[{"given":"Jaime","family":"Arias","sequence":"first","affiliation":[]},{"given":"Wojciech","family":"Jamroga","sequence":"additional","affiliation":[]},{"given":"Wojciech","family":"Penczek","sequence":"additional","affiliation":[]},{"given":"Laure","family":"Petrucci","sequence":"additional","affiliation":[]},{"given":"Teofil","family":"Sidoruk","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2026,2,9]]},"reference":[{"issue":"1","key":"9726_CR1","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1007\/s10849-008-9075-4","volume":"18","author":"T \u00c5gotnes","year":"2009","unstructured":"\u00c5gotnes, T., & Walther, D. (2009). A logic of strategic ability under bounded memory. Journal of Logic, Language and Information, 18(1), 55\u201377.","journal-title":"Journal of Logic, Language and Information"},{"key":"9726_CR2","doi-asserted-by":"crossref","unstructured":"\u00c5gotnes, T., Goranko, V., & Jamroga, W. (2007). Alternating-time temporal logics with irrevocable strategies. In Proceedings of the 11th conference on Theoretical Aspects of Rationality and Knowledge (TARK \u201907). ACM, New York, NY, USA, pp. 15\u201324.","DOI":"10.1145\/1324249.1324256"},{"key":"9726_CR3","first-page":"543","volume-title":"Handbook of epistemic logic","author":"T \u00c5gotnes","year":"2015","unstructured":"\u00c5gotnes, T., Goranko, V., Jamroga, W., et al. (2015). Knowledge and ability. Handbook of epistemic logic (pp. 543\u2013589). Rickmansworth, UK: College Publications."},{"key":"9726_CR4","doi-asserted-by":"publisher","first-page":"126","DOI":"10.1016\/j.jcss.2017.03.008","volume":"88","author":"N Alechina","year":"2017","unstructured":"Alechina, N., Logan, B., Nguyen, H. N., et al. (2017). Model-checking for resource-bounded ATL with production and consumption of resources. Journal of Computer and System Sciences, 88, 126\u2013144.","journal-title":"Journal of Computer and System Sciences"},{"key":"9726_CR5","doi-asserted-by":"crossref","unstructured":"Alechina, N., Demri, S., & Logan, B. (2020). Parameterised resource-bounded ATL. In Proceedings of AAAI 2020. AAAI Press, pp. 7040\u20137046.","DOI":"10.1609\/aaai.v34i05.6189"},{"key":"9726_CR6","doi-asserted-by":"crossref","unstructured":"Alur, R., & Dill, D. L. (1990). Automata for modeling real-time systems. In Proceedings of the 17th International Colloquium on Automata, Languages and Programming, ICALP90, Lecture Notes in Computer Science, vol. 443. Springer, Berlin, Germany, pp 322\u2013335.","DOI":"10.1007\/BFb0032042"},{"issue":"1","key":"9726_CR7","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1006\/inco.1993.1024","volume":"104","author":"R Alur","year":"1993","unstructured":"Alur, R., Courcoubetis, C., & Dill, D. L. (1993). Model-checking in dense real-time. Information and Computation, 104(1), 2\u201334.","journal-title":"Information and Computation"},{"key":"9726_CR8","doi-asserted-by":"publisher","unstructured":"Alur, R., Henzinger, T., & Vardi, M. (1993). Parametric real-time reasoning. In ACM Symposium on Theory of Computing, 1993. ACM, pp. 592\u2013601. https:\/\/doi.org\/10.1145\/167088.167242","DOI":"10.1145\/167088.167242"},{"key":"9726_CR9","doi-asserted-by":"crossref","unstructured":"Alur, R., Henzinger, T. A., & Kupferman, O. (1997). Alternating-time temporal logic. In Proceedings of the 38th annual symposium on Foundations of Computer Science (FOCS \u201997). IEEE Computer Society, Palo Alto, CA, USA, pp. 100\u2013109.","DOI":"10.1109\/SFCS.1997.646098"},{"key":"9726_CR10","doi-asserted-by":"crossref","unstructured":"Alur, R., Henzinger, T., Kupferman, O., et\u00a0al. (1998). Alternating refinement relations. In Proceedings of the 9th international conference on Concurrency Theory, CONCUR \u201998, Lecture Notes in Computer Science, vol. 1466. Springer, Berlin, Germany, pp. 163\u2013178.","DOI":"10.1007\/BFb0055622"},{"key":"9726_CR11","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. (2002). Alternating-time Temporal Logic. Journal of the ACM, 49, 672\u2013713.","journal-title":"Journal of the ACM"},{"key":"9726_CR12","doi-asserted-by":"crossref","unstructured":"Andr\u00e9, \u00c9., Fribourg, L., K\u00fchne, U., et\u00a0al. (2012). IMITATOR 2.5: A tool for analyzing robustness in scheduling problems. In FM\u00a02012, Lecture Notes in Computer Science, vol. 7436. Springer, Berlin, Germany, pp. 33\u201336.","DOI":"10.1007\/978-3-642-32759-9_6"},{"key":"9726_CR13","doi-asserted-by":"crossref","unstructured":"Andr\u00e9, \u00c9., Knapik, M., Penczek, W., et\u00a0al. (2016). Controlling actions and time in parametric timed automata. In Proc. 16th Int. Conf. on Application of Concurrency to System Design (ACSD\u201916), Toru\u0144, Poland. IEEE, pp. 45\u201354.","DOI":"10.1109\/ACSD.2016.20"},{"key":"9726_CR14","doi-asserted-by":"crossref","unstructured":"Andr\u00e9, \u00c9., Knapik, M., Lime, D., et al. (2019). Parametric verification: An introduction. Transactions on Petri Nets and Other Models of Concurrency (vol. 14, pp. 64\u2013100).","DOI":"10.1007\/978-3-662-60651-3_3"},{"key":"9726_CR15","doi-asserted-by":"crossref","unstructured":"Arias, J., Jamroga, W., Penczek, W., et\u00a0al. (2023). Strategic (timed) computation tree logic. In Proceedings of AAMAS 2023. ACM, pp. 382\u2013390.","DOI":"10.65109\/KJPV9098"},{"key":"9726_CR16","doi-asserted-by":"crossref","unstructured":"Berthon, R., Maubert, B., Murano, A., et\u00a0al. (2017). Strategy logic with imperfect information. In Proceedings of LICS, pp. 1\u201312.","DOI":"10.1109\/LICS.2017.8005136"},{"key":"9726_CR17","doi-asserted-by":"crossref","unstructured":"Beutner, R., & Finkbeiner, B. (2023). Hyperatl*: A logic for hyperproperties in multi-agent systems. Logical Methods in Computer Science, 19(2).","DOI":"10.46298\/lmcs-19(2:13)2023"},{"key":"9726_CR18","doi-asserted-by":"publisher","first-page":"323","DOI":"10.1016\/j.entcs.2009.02.044","volume":"231","author":"P Bouyer","year":"2009","unstructured":"Bouyer, P. (2009). Model-checking timed temporal logics. Electronic Notes in Theoretical Computer Science, 231, 323\u2013341.","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"9726_CR19","doi-asserted-by":"crossref","unstructured":"Brihaye, T., Lopes, A. D. C., Laroussinie, F., et\u00a0al. (2009). ATL with strategy contexts and bounded memory. In Proceedings of LFCS, Lecture Notes in Computer Science, vol. 5407. Springer, pp. 92\u2013106.","DOI":"10.1007\/978-3-540-92687-0_7"},{"key":"9726_CR20","doi-asserted-by":"crossref","unstructured":"Bulling, N., Goranko, V., & Jamroga, W. (2015). Logics for reasoning about strategic abilities in multi-player games. In Models of strategic reasoning. Logics, games, and communities, Lecture Notes in Computer Science, vol. 8972. Springer, Berlin, Germany, pp. 93\u2013136.","DOI":"10.1007\/978-3-662-48540-8_4"},{"key":"9726_CR21","doi-asserted-by":"crossref","unstructured":"Burch, J. R., Clarke, E. M., McMillan, K. L., et\u00a0al. (1990). Sequential circuit verification using symbolic model checking. In Proceedings of the 27th ACM\/IEEE design automation conference. IEEE Computer Society Press, pp. 46\u201351.","DOI":"10.1145\/123186.123223"},{"key":"9726_CR22","doi-asserted-by":"crossref","unstructured":"Chatterjee, K., Henzinger, T. A., & Piterman, N. (2007). Strategy logic. In Proceedings of CONCUR, pp. 59\u201373.","DOI":"10.1007\/978-3-540-74407-8_5"},{"key":"9726_CR23","unstructured":"Christoffersen, P., Hansen, M., Mariegaard, A., et\u00a0al. (2015). Parametric verification of weighted systems. In Proceedings of SynCoP 2015, OASIcs, vol.\u00a044. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, pp, 77\u201390."},{"issue":"4","key":"9726_CR24","doi-asserted-by":"publisher","first-page":"443","DOI":"10.1145\/363516.363528","volume":"9","author":"EM Clarke","year":"2000","unstructured":"Clarke, E. M., Jha, S., & Marrero, W. R. (2000). Verifying security protocols with Brutus. ACM Transactions on Software Engineering and Methodology, 9(4), 443\u2013487.","journal-title":"ACM Transactions on Software Engineering and Methodology"},{"key":"9726_CR25","unstructured":"Dima, C., & Tiplea, F. (2011). Model-checking ATL under imperfect information and perfect recall semantics is undecidable. CoRR. arXiv:1102.4225, pp. 1\u201317."},{"key":"9726_CR26","doi-asserted-by":"crossref","unstructured":"Faella, M, Torre, S. L., & Murano, A. (2002). Dense real-time games. In Proceedings of the 17th IEEE symposium on Logic in Computer Science (LICS 2002). IEEE Computer Society, Palo Alto, CA, USA, pp. 167\u2013176.","DOI":"10.1109\/LICS.2002.1029826"},{"key":"9726_CR27","doi-asserted-by":"publisher","first-page":"46","DOI":"10.1016\/j.tcs.2013.08.021","volume":"515","author":"M Faella","year":"2014","unstructured":"Faella, M., La Torre, S., & Murano, A. (2014). Automata-theoretic decision of timed games. Theoretical Computer Science, 515, 46\u201363.","journal-title":"Theoretical Computer Science"},{"key":"9726_CR28","doi-asserted-by":"publisher","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., et al. (1995). Reasoning about knowledge. Cambridge, MA, USA: MIT Press."},{"issue":"2","key":"9726_CR29","doi-asserted-by":"publisher","first-page":"241","DOI":"10.1023\/B:SYNT.0000024915.66183.d1","volume":"139","author":"V Goranko","year":"2004","unstructured":"Goranko, V., & Jamroga, W. (2004). Comparing semantics of logics for multi-agent systems. Synthese, 139(2), 241\u2013280.","journal-title":"Synthese"},{"key":"9726_CR30","doi-asserted-by":"crossref","unstructured":"Guelev, D., & Dima, C. (2012). Epistemic ATL with perfect recall, past and strategy contexts. In Proceedings of CLIMA-XIII, Lecture Notes in Computer Science, vol. 7486. Springer, pp. 77\u201393.","DOI":"10.1007\/978-3-642-32897-8_7"},{"key":"9726_CR31","doi-asserted-by":"crossref","unstructured":"Havelund, K., & Shankar, N. (1996). Experiments in theorem proving and model checking for protocol verification. In Proceedings of FME \u201996. Springer, Berlin, pp. 662\u2013681.","DOI":"10.1007\/3-540-60973-3_113"},{"issue":"8","key":"9726_CR32","doi-asserted-by":"publisher","first-page":"749","DOI":"10.1109\/32.940728","volume":"27","author":"K Havelund","year":"2001","unstructured":"Havelund, K., Lowry, M., & Penix, J. (2001). Formal analysis of a space craft controller using SPIN. IEEE Transactions on Software Engineering, 27(8), 749\u2013765.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"9726_CR33","doi-asserted-by":"crossref","unstructured":"Holzmann, G. J., & Joshi, R. (2004). Model-driven software verification. In Proceedings of the 11th International SPIN Workshop, Lecture Notes in Computer Science, vol. 2989. Springer, pp. 76\u201391.","DOI":"10.1007\/978-3-540-24732-6_6"},{"key":"9726_CR34","doi-asserted-by":"crossref","unstructured":"Huang, X., & van\u00a0der Meyden, R. (2014). Symbolic model checking epistemic strategy logic. In Proceedings of the 28th AAAI Conference on Artificial Intelligence (AAAI14). AAAI Press, Palo Alto, CA, USA, pp. 1426\u20131432.","DOI":"10.1609\/aaai.v28i1.8894"},{"key":"9726_CR35","doi-asserted-by":"crossref","unstructured":"Jamroga, W. (2008). Knowledge and strategic ability for model checking: A refined approach. In Proceedings of the 6th German conference on Multiagent Systems Technologies, MATES 2008, Lecture Notes in Computer Science, vol. 5244. Springer, Berlin, Germany, pp. 99\u2013110.","DOI":"10.1007\/978-3-540-87805-6_10"},{"key":"9726_CR36","volume-title":"Logical methods for specification and verification of multi-agent systems","author":"W Jamroga","year":"2015","unstructured":"Jamroga, W. (2015). Logical methods for specification and verification of multi-agent systems. Warsaw, Poland: ICS PAS Publishing House."},{"key":"9726_CR37","unstructured":"Jamroga, W., & Bulling, N. (2011). Comparing variants of strategic ability. In Proceedings of IJCAI\u201911, pp. 252\u2013257."},{"key":"9726_CR38","unstructured":"Jamroga, W., & Dix, J. (2006). Model checking ATL$$_{ir}$$ is indeed $$\\Delta _2^P$$-complete. In Proceedings of the 4th European Workshop on Multi-Agent Systems, EUMAS \u201906, CEUR Workshop Proceedings (vol. 223). CEUR-WS.org, Aachen, Germany, pp. 13\u201324."},{"key":"9726_CR39","doi-asserted-by":"crossref","unstructured":"Jamroga, W., van\u00a0der Hoek, W., & Wooldridge, M. (2005). Intentions and strategies in game-like scenarios. In Bento, C., Cardoso, A., & Dias, G. (Eds.), Progress in artificial intelligence: Proceedings of EPIA 2005, Lecture Notes in Artificial Intelligence, vol. 3808. Springer, pp. 512\u2013523.","DOI":"10.1007\/11595014_51"},{"key":"9726_CR40","doi-asserted-by":"crossref","unstructured":"Jamroga, W., Konikowska, B., & Penczek, W. (2016). Multi-valued verification of strategic ability. In Proceedings of the 15th international conference on Autonomous Agents and Multiagent Systems (AAMAS 2016). ACM, New York, NY, USA, pp. 1180\u20131189.","DOI":"10.65109\/ORTV4675"},{"key":"9726_CR41","doi-asserted-by":"crossref","unstructured":"Jamroga, W., Penczek, W., Dembinski, P., et\u00a0al. (2018.) Towards partial order reductions for strategic ability. In Proceedings of the 17th international conference on autonomous agents and multiagent systems. IFAAMAS, Richland, SC, USA, AAMAS 2018, pp. 156\u2013165.","DOI":"10.65109\/ALPX5612"},{"key":"9726_CR42","doi-asserted-by":"crossref","unstructured":"Jamroga, W., Malvone, V., & Murano, A. (2019). Natural strategic ability. Artificial Intelligence, 277.","DOI":"10.1016\/j.artint.2019.103170"},{"key":"9726_CR43","doi-asserted-by":"publisher","first-page":"817","DOI":"10.1613\/jair.1.11936","volume":"68","author":"W Jamroga","year":"2020","unstructured":"Jamroga, W., Penczek, W., Sidoruk, T., et al. (2020). Towards partial order reductions for strategic ability. JAIR, 68, 817\u2013850.","journal-title":"JAIR"},{"key":"9726_CR44","doi-asserted-by":"crossref","unstructured":"Kacprzak, M., & Penczek, W. (2004). Unbounded model checking for alternating-time temporal logic. In Proceedings of the 3rd international joint conference on Autonomous Agents and Multiagent Systems (AAMAS 2004). IEEE Computer Society, Palo Alto, CA, USA, pp. 646\u2013653.","DOI":"10.65109\/PDYS8617"},{"issue":"1","key":"9726_CR45","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. (2005). Fully symbolic unbounded model checking for alternating-time temporal logic. Autonomous Agents and Multi-Agent Systems, 11(1), 69\u201389.","journal-title":"Autonomous Agents and Multi-Agent Systems"},{"key":"9726_CR46","doi-asserted-by":"crossref","unstructured":"Kacprzak, M., Niewiadomski, A., & Penczek, W. (2021). Satisfiability checking of strategy logic with simple goals. In Proceedings of the 18th international conference on principles of knowledge representation and reasoning, KR 2021 (pp. 400\u2013410).","DOI":"10.24963\/kr.2021\/38"},{"key":"9726_CR47","doi-asserted-by":"crossref","unstructured":"Kaminski, M., Kurpiewski, D., & Jamroga, W. (2024). STV+KH: Towards practical verification of strategic ability for knowledge and information flow. In Proceedings of AAMAS 2024. International foundation for autonomous agents and multiagent systems\/ACM (pp. 2812\u20132814).","DOI":"10.65109\/LILV1577"},{"key":"9726_CR48","doi-asserted-by":"crossref","unstructured":"Kaminski, M., Kurpiewski, D., & Jamroga, W. (2025). Natstv: Towards verification of natural strategic ability. In Proceedings of IJCAI 2025. ijcai.org, pp. 11072\u201311076.","DOI":"10.24963\/ijcai.2025\/1265"},{"key":"9726_CR49","doi-asserted-by":"crossref","unstructured":"Kim, Y., Jamroga, W., Penczek, W., et\u00a0al. (2025). Practical abstractions for model checking continuous-time multi-agent systems. In Proceedings of AAMAS 2025. ACM, pp. 1117\u20131126.","DOI":"10.65109\/SAGI5833"},{"key":"9726_CR50","doi-asserted-by":"publisher","first-page":"197","DOI":"10.1613\/jair.1.11612","volume":"66","author":"M Knapik","year":"2019","unstructured":"Knapik, M., Andr\u00e9, \u00c9., Petrucci, L., et al. (2019). Timed ATL: Forget memory, just count. Journal of Artificial Intelligence Research, 66, 197\u2013223.","journal-title":"Journal of Artificial Intelligence Research"},{"key":"9726_CR51","unstructured":"Kouvaros, P., & Lomuscio, A. (2016). Parameterised model checking for alternating-time temporal logic. In Proceedings of ECAI 2016, frontiers in artificial intelligence and applications (vol. 285). IOS Press, pp. 1230\u20131238."},{"issue":"2","key":"9726_CR52","doi-asserted-by":"publisher","first-page":"322","DOI":"10.1006\/inco.2000.2893","volume":"164","author":"O Kupferman","year":"2001","unstructured":"Kupferman, O., Vardi, M. Y., & Wolper, P. (2001). Module checking. Information and Computation, 164(2), 322\u2013344.","journal-title":"Information and Computation"},{"key":"9726_CR53","unstructured":"Kurpiewski, D., Jamroga, W., Ma\u015bko, \u0141., et\u00a0al. (2022). Verification of multi-agent properties in electronic voting: A case study. In Proceedings of AiML 2022. College Publications, pp. 531\u2013556."},{"key":"9726_CR54","doi-asserted-by":"crossref","unstructured":"Kurpiewski, D., Jamroga, W., & Sidoruk, T. (2023). Towards modelling and verification of social explainable AI. In Proceedings of ICAART 2023. SCITEPRESS, pp. 396\u2013403.","DOI":"10.5220\/0011799900003393"},{"key":"9726_CR55","doi-asserted-by":"crossref","unstructured":"Kurpiewski, D., Kim, Y., & Jamroga, W. (2025). Approximate verification of strategic abilities under imperfect information using local models. In Proceedings of IJCAI 2025, to appear.","DOI":"10.24963\/ijcai.2025\/17"},{"issue":"1\u20132","key":"9726_CR56","doi-asserted-by":"publisher","first-page":"188","DOI":"10.1007\/s10703-020-00356-y","volume":"58","author":"M Kwiatkowska","year":"2021","unstructured":"Kwiatkowska, M., Norman, G., Parker, D., et al. (2021). Automatic verification of concurrent stochastic systems. Formal Methods in System Design, 58(1\u20132), 188\u2013250.","journal-title":"Formal Methods in System Design"},{"key":"9726_CR57","doi-asserted-by":"publisher","first-page":"98","DOI":"10.1016\/j.ic.2014.12.020","volume":"245","author":"F Laroussinie","year":"2015","unstructured":"Laroussinie, F., & Markey, N. (2015). Augmenting ATL with strategy contexts. Information and Computation, 245, 98\u2013123.","journal-title":"Information and Computation"},{"key":"9726_CR58","doi-asserted-by":"crossref","unstructured":"Laroussinie, F., Markey, N., & Oreiby, G. (2006). Model-checking timed ATL for durational concurrent game structures. In Proceedings of the 4th international conference on Formal Modeling and Analysis of Timed Systems, FORMATS 2006, Lecture Notes in Computer Science, vol. 4202. Springer, Berlin, Germany, pp. 245\u2013259.","DOI":"10.1007\/11867340_18"},{"key":"9726_CR59","doi-asserted-by":"crossref","unstructured":"Lomuscio, A., & Ryan, M. (1997). On the relation between interpreted systems and Kripke models. In Agents and multi-agent systems formalisms, methodologies, and applications, Lecture Notes in Artificial Intelligence, vol. 1441. Berlin, Germany: Springer, pp. 46\u201359.","DOI":"10.1007\/BFb0055019"},{"key":"9726_CR60","doi-asserted-by":"crossref","unstructured":"Lomuscio, A., Penczek, W., & Qu, H. (2010). Partial order reductions for model checking temporal epistemic logics over interleaved multi-agent systems. In AAMAS 2010, vol. 1\u20133, Richland, SC, USA: IFAAMAS pp. 659\u2013666.","DOI":"10.65109\/LUOO1481"},{"issue":"1\u20132","key":"9726_CR61","doi-asserted-by":"publisher","first-page":"71","DOI":"10.3233\/FI-2010-276","volume":"101","author":"A Lomuscio","year":"2010","unstructured":"Lomuscio, A., Penczek, W., & Qu, H. (2010). Partial order reductions for model checking temporal-epistemic logics over interleaved multi-agent systems. Fundamenta Informaticae, 101(1\u20132), 71\u201390.","journal-title":"Fundamenta Informaticae"},{"key":"9726_CR62","first-page":"84","volume":"24","author":"A Lomuscio","year":"2015","unstructured":"Lomuscio, A., Qu, H., & Raimondi, F. (2015). MCMAS: An open-source model checker for the verification of multi-agent systems. International Journal on Software Tools for Technology Transfer, 24, 84\u201390.","journal-title":"International Journal on Software Tools for Technology Transfer"},{"key":"9726_CR63","unstructured":"Mogavero, F., Murano, A., & Vardi, M. (2010). Reasoning about strategies. In Proceedings of FSTTCS, pp. 133\u2013144."},{"issue":"4","key":"9726_CR64","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2631917","volume":"15","author":"F Mogavero","year":"2014","unstructured":"Mogavero, F., Murano, A., Perelli, G., et al. (2014). Reasoning about strategies: On the model-checking problem. ACM Transactions on Computational Logic, 15(4), 1\u201342.","journal-title":"ACM Transactions on Computational Logic"},{"key":"9726_CR65","doi-asserted-by":"crossref","unstructured":"Penczek, W., & Polrola, A. (2006). Advances in verification of time petri nets and timed automata: A temporal logic approach, studies in computational intelligence, (vol. 20). Springer.","DOI":"10.1007\/978-3-540-32870-4"},{"key":"9726_CR66","doi-asserted-by":"crossref","unstructured":"Pilecki, J., Bednarczyk, M., & Jamroga, W. (2014). Synthesis and verification of uniform strategies for multi-agent systems. In Proceedings of CLIMA XV, Lecture Notes in Computer Science, vol. 8624. Springer, pp. 166\u2013182.","DOI":"10.1007\/978-3-319-09764-0_11"},{"key":"9726_CR67","doi-asserted-by":"crossref","unstructured":"Schneider, F., Easterbrook, S. M., Callahan, J. R., et\u00a0al. (1998). Validating requirements for fault tolerant systems using model checking. In Proceedings of ICRE \u201998. IEEE Computer Society, pp. 4\u201313.","DOI":"10.1109\/ICRE.1998.667803"},{"key":"9726_CR68","doi-asserted-by":"crossref","unstructured":"Schobbens, P. Y. (2004). Alternating-time logic with imperfect recall. In 1st International workshop on Logic and Communication in Multi-Agent Systems (LCMAS 2003), Electronic Notes in Theoretical Computer Science, vol. 85. Amsterdam: Elsevier, pp. 1\u201312.","DOI":"10.1016\/S1571-0661(05)82604-0"},{"key":"9726_CR69","doi-asserted-by":"crossref","unstructured":"Springall, D., Finkenauer, T., Durumeric, Z., et\u00a0al. (2014). Security analysis of the Estonian internet voting system. In Proceedings of the 2014 ACM SIGSAC conference on Computer and Communications Security (CCS \u201914). ACM, New York, NY, USA, pp. 703\u2013715.","DOI":"10.1145\/2660267.2660315"},{"key":"9726_CR70","doi-asserted-by":"crossref","unstructured":"Tabatabaei, M., & Jamroga, W. (2023). Playing to learn, or to keep secret: Alternating-time logic meets information theory. In Proceedings of AAMAS\u201923. ACM, pp. 766\u2013774.","DOI":"10.65109\/PVIG7394"},{"key":"9726_CR71","doi-asserted-by":"crossref","unstructured":"van\u00a0der Hoek, W., Jamroga, W., & Wooldridge, M. (2005). A logic for strategic reasoning. In Proceedings of AAMAS\u201905 (pp. 157\u2013164).","DOI":"10.1145\/1082473.1082497"},{"key":"9726_CR72","doi-asserted-by":"crossref","unstructured":"Walther, D., van\u00a0der Hoek, W., & Wooldridge, M. (2007). Alternating-time temporal logic with explicit strategies. In Samet, D. (Ed.), Proceedings TARK XI. Presses Universitaires de Louvain, pp. 269\u2013278.","DOI":"10.1145\/1324249.1324285"},{"key":"9726_CR73","unstructured":"Wang, Y., & Dechesne, F. (2009). On expressive power and class invariance. CoRR. arXiv:0905.4332, pp. 1\u201318."},{"key":"9726_CR74","doi-asserted-by":"crossref","unstructured":"Witkowski, T., Blanc, N., Kroening, D., et\u00a0al. (2007). Model checking concurrent Linux device drivers. In Proceedings of ASE \u201907. ACM, pp. 501\u2013504.","DOI":"10.1145\/1321631.1321719"}],"container-title":["Autonomous Agents and Multi-Agent Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10458-025-09726-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10458-025-09726-4","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10458-025-09726-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,2,9]],"date-time":"2026-02-09T10:35:45Z","timestamp":1770633345000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10458-025-09726-4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,2,9]]},"references-count":74,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2026,6]]}},"alternative-id":["9726"],"URL":"https:\/\/doi.org\/10.1007\/s10458-025-09726-4","relation":{},"ISSN":["1387-2532","1573-7454"],"issn-type":[{"value":"1387-2532","type":"print"},{"value":"1573-7454","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026,2,9]]},"assertion":[{"value":"30 October 2023","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"4 November 2025","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"9 February 2026","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Declarations"}},{"value":"The authors declare no competing interests.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Competing Interests"}}],"article-number":"7"}}