{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,9]],"date-time":"2026-07-09T17:52:58Z","timestamp":1783619578604,"version":"3.55.0"},"reference-count":84,"publisher":"Springer Science and Business Media LLC","issue":"9","license":[{"start":{"date-parts":[[2021,8,3]],"date-time":"2021-08-03T00:00:00Z","timestamp":1627948800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2021,8,3]],"date-time":"2021-08-03T00:00:00Z","timestamp":1627948800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Appl Intell"],"published-print":{"date-parts":[[2021,9]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We provide a survey of the state of the art of<jats:italic>rational verification<\/jats:italic>: the problem of checking whether a given temporal logic formula<jats:italic>\u03d5<\/jats:italic>is satisfied in some or all game-theoretic equilibria of a multi-agent system \u2013 that is, whether the system will exhibit the behavior<jats:italic>\u03d5<\/jats:italic>represents under the assumption that agents within the system act rationally in pursuit of their preferences. After motivating and introducing the overall framework of rational verification, we discuss key results obtained in the past few years as well as relevant related work in logic, AI, and computer science.<\/jats:p>","DOI":"10.1007\/s10489-021-02658-y","type":"journal-article","created":{"date-parts":[[2021,8,3]],"date-time":"2021-08-03T11:02:51Z","timestamp":1627988571000},"page":"6569-6584","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":16,"title":["Rational verification: game-theoretic verification of multi-agent systems"],"prefix":"10.1007","volume":"51","author":[{"given":"Alessandro","family":"Abate","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Julian","family":"Gutierrez","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Lewis","family":"Hammond","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Paul","family":"Harrenstein","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Marta","family":"Kwiatkowska","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Muhammad","family":"Najib","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Giuseppe","family":"Perelli","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Thomas","family":"Steeples","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9329-8410","authenticated-orcid":false,"given":"Michael","family":"Wooldridge","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2021,8,3]]},"reference":[{"key":"2658_CR1","doi-asserted-by":"crossref","unstructured":"Almagor S, Boker U, Kupferman O (2013) Formalizing and reasoning about quality. In: Fomin FV, Freivalds R, Kwiatkowska MZ, Peleg D (eds) Automata, Languages, and Programming - 40th International Colloquium, ICALP 2013, Proceedings, Part II, volume 7966 of Lecture Notes in Computer Science. Springer, Riga, pp 15\u201327","DOI":"10.1007\/978-3-642-39212-2_3"},{"key":"2658_CR2","doi-asserted-by":"crossref","unstructured":"Almagor S, Kupferman O, Perelli G (2018) Synthesis of controllable nash equilibria in quantitative objective games. In: Proceedings of the 27th International Joint Conference on Artificial Intelligence, IJCAI\u201918. AAAI Press, pp 35\u201341","DOI":"10.24963\/ijcai.2018\/5"},{"issue":"11","key":"2658_CR3","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1023\/A:1008739929481","volume":"15","author":"R Alur","year":"1999","unstructured":"Alur R, Henzinger TA (1999) Reactive modules. Formal Methods Syst Des 15(11):7\u201348","journal-title":"Formal Methods Syst Des"},{"key":"2658_CR4","doi-asserted-by":"crossref","unstructured":"Alur R, Henzinger TA, Kupferman O (1997) Alternating-time temporal logic. In: Proceedings of the 38th IEEE Symposium on Foundations of Computer Science, Florida, pp 100\u2013109","DOI":"10.1109\/SFCS.1997.646098"},{"issue":"5","key":"2658_CR5","doi-asserted-by":"publisher","first-page":"672","DOI":"10.1145\/585265.585270","volume":"49","author":"R Alur","year":"2002","unstructured":"Alur R, Henzinger TA, Kupferman O (2002) Alternating-time temporal logic. J ACM 49 (5):672\u2013713","journal-title":"J ACM"},{"key":"2658_CR6","doi-asserted-by":"crossref","unstructured":"Alur R, Henzinger TA, Kupferman O, Vardi MY (1998) Alternating refinement relations. In: Proceedings of the 9th International Conference on Concurrency Theory (CONCUR\u201998), volume 1466 of Lecture Notes in Computer Science. Springer, Berlin, pp 163\u2013178","DOI":"10.1007\/BFb0055622"},{"issue":"1","key":"2658_CR7","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/963927.963928","volume":"5","author":"R Alur","year":"2004","unstructured":"Alur R, Torre SL (2004) Deterministic generators and games for ltl fragments. ACM Trans Comput Log (TOCL) 5(1):1\u201325","journal-title":"ACM Trans Comput Log (TOCL)"},{"key":"2658_CR8","doi-asserted-by":"crossref","unstructured":"Aminof B, Kwiatkowska M, Maubert B, Murano A, Rubin S (2019) Probabilistic strategy logic. In: In Proc. International Joint Conference on Artificial Intelligence (IJCAI-19)","DOI":"10.24963\/ijcai.2019\/5"},{"key":"2658_CR9","unstructured":"Baier C, Katoen J-P (2008) Principles Of model checking. The MIT Press, Cambridge"},{"key":"2658_CR10","doi-asserted-by":"crossref","unstructured":"Baier C, Haverkort B, Hermanns H, Katoen J-P (2000) Model checking continuous-time markov chains by transient analysis. In: Computer Aided Verification. Springer, Berlin, pp 358\u2013372","DOI":"10.1007\/10722167_28"},{"key":"2658_CR11","doi-asserted-by":"crossref","unstructured":"Basset N, Kwiatkowska M, Topcu U, Wiltsche C (2015) Strategy synthesis for stochastic games with multiple long-run objectives. In: Tools and Algorithms for the Construction and Analysis of Systems. Berlin, Springer, pp 256\u2013271","DOI":"10.1007\/978-3-662-46681-0_22"},{"issue":"3","key":"2658_CR12","doi-asserted-by":"publisher","first-page":"911","DOI":"10.1016\/j.jcss.2011.08.007","volume":"78","author":"R Bloem","year":"2012","unstructured":"Bloem R, Jobstmann B, Piterman N, Pnueli A, Sa\u2019ar Y (2012) Synthesis of Reactive (1) designs. J Comput Syst Sci 78(3):911\u2013938","journal-title":"J Comput Syst Sci"},{"key":"2658_CR13","doi-asserted-by":"crossref","unstructured":"Bouyer P, Brenguier R, Markey N, Ummels M (2015) Pure Nash equilibria in concurrent deterministic games. Logical Methods in Computer Science","DOI":"10.2168\/LMCS-11(2:9)2015"},{"key":"2658_CR14","unstructured":"Boyer R. S., Moore J. S. (eds) (1981) The Correctness Problem in Computer Science. The Academic Press, London"},{"key":"2658_CR15","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1016\/j.artint.2012.08.005","volume":"198","author":"R Brafman","year":"2013","unstructured":"Brafman R, Domshlak C (2013) On the complexity of planning for agent teams and its implications for single agent planning. Artif Intell 198:52\u201371","journal-title":"Artif Intell"},{"key":"2658_CR16","doi-asserted-by":"crossref","unstructured":"Br\u00e1zdil T, Chatterjee K, Chmel\u00edk M, Forejt V, K\u0159et\u00ednsk\u00fd J, Kwiatkowska M, Parker D, Ujma M (2014) Verification of markov decision processes using learning algorithms. In: Automated Technology for Verification and Analysis. Springer International Publishing, pp 98\u2013114","DOI":"10.1007\/978-3-319-11936-6_8"},{"key":"2658_CR17","doi-asserted-by":"crossref","unstructured":"Calude CS, Jain S, Khoussainov B, Li W, Stephan F (2017) Deciding parity games in quasipolynomial time. In: STOC. ACM, pp 252\u2013263","DOI":"10.1145\/3055399.3055409"},{"key":"2658_CR18","doi-asserted-by":"crossref","unstructured":"\u010cerm\u00e1k P, Lomuscio A, Mogavero F, Murano A (2014) Mcmas-slk: A model checker for the verification of strategy logic specifications. In: Biere A., Bloem R. (eds) Computer Aided Verification. Springer International Publishing, Cham, pp 525\u2013532","DOI":"10.1007\/978-3-319-08867-9_34"},{"issue":"Part","key":"2658_CR19","doi-asserted-by":"publisher","first-page":"588","DOI":"10.1016\/j.ic.2017.09.011","volume":"261","author":"P Cerma\u0307k","year":"2018","unstructured":"Cerma\u0307k P, Lomuscio A, Mogavero F, Murano (2018) Practical verification of multi-agent systems against slk specifications. Inf Comput 261(Part):588\u2013614","journal-title":"Inf Comput"},{"key":"2658_CR20","doi-asserted-by":"crossref","unstructured":"Chalkiadakis G, Elkind E, Wooldridge M (2011) Computational aspects of cooperative game theory. Morgan-Claypool","DOI":"10.2200\/S00355ED1V01Y201107AIM016"},{"issue":"1","key":"2658_CR21","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1002\/(SICI)1097-024X(199601)26:1<105::AID-SPE3>3.0.CO;2-#","volume":"26","author":"TS Chan","year":"1996","unstructured":"Chan TS, Gorton I (1996) Formal validation of a high performance error control protocol using spin. Softw Practice Exper 26(1):105\u2013124","journal-title":"Softw Practice Exper"},{"issue":"2","key":"2658_CR22","doi-asserted-by":"publisher","first-page":"394","DOI":"10.1016\/j.jcss.2011.05.002","volume":"78","author":"K Chatterjee","year":"2012","unstructured":"Chatterjee K, Henzinger TA (2012) A survey of stochastic \u03c9-regular games. J Comput Syst Sci 78(2):394\u2013413","journal-title":"J Comput Syst Sci"},{"key":"2658_CR23","doi-asserted-by":"crossref","unstructured":"Chatterjee K, Henzinger TA, Jurdzinski M (2005) Mean-payoff parity games. In: 20th Annual IEEE Symposium on Logic in Computer Science (LICS\u201905). IEEE, pp 178\u2013187","DOI":"10.1109\/LICS.2005.26"},{"issue":"6","key":"2658_CR24","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 TA, Piterman N (2010) Strategy logic. Inf Comput 208(6):677\u2013693. https:\/\/doi.org\/10.1016\/j.ic.2009.07.004","journal-title":"Inf Comput"},{"issue":"1","key":"2658_CR25","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1007\/s10703-013-0183-7","volume":"43","author":"T Chen","year":"2013","unstructured":"Chen T, Forejt V, Kwiatkowska M, Parker D (2013) Simaitis, A Automatic verification of competitive stochastic systems. Formal Methods Syst Des 43(1):61\u201392","journal-title":"Formal Methods Syst Des"},{"issue":"3","key":"2658_CR26","doi-asserted-by":"publisher","first-page":"199","DOI":"10.1007\/s10703-006-0027-9","volume":"30","author":"Y Choi","year":"2007","unstructured":"Choi Y (2007) From NuSMV to SPIN: Experiences with model checking flight guidance systems. Formal Methods Syst Des 30(3):199\u2013216","journal-title":"Formal Methods Syst Des"},{"key":"2658_CR27","doi-asserted-by":"crossref","unstructured":"Clarke EM, Emerson EA (1981) Design and synthesis of synchronization skeletons using branching time temporal logic. In: Logics of Programs \u2014 Proceedings 1981 (LNCS Volume 131). Springer, Berlin, pp 52\u201371","DOI":"10.1007\/BFb0025774"},{"key":"2658_CR28","unstructured":"Clarke EM, Grumberg O, Peled DA (2000) Model the Checking. MIT press, Cambridge"},{"key":"2658_CR29","unstructured":"de Alfaro L, Henzinger TA (2000) Concurrent omega-regular games. In: Proceedings of the 15th Annual IEEE Symposium on Logic in Computer Science, LICS \u201900. IEEE Computer Society, USA, pp 141"},{"key":"2658_CR30","doi-asserted-by":"crossref","unstructured":"Downey RG, Fellows MR (1999) Parameterized complexity. Springer, New York","DOI":"10.1007\/978-1-4612-0515-9"},{"key":"2658_CR31","doi-asserted-by":"crossref","unstructured":"Emerson EA (1990) Temporal and modal logic. In: Handbook of Theoretical Computer Science Volume B: Formal Models and Semantics. Amsterdam, Elsevier Science Publishers B.V., pp 996\u20131072","DOI":"10.1016\/B978-0-444-88074-1.50021-4"},{"key":"2658_CR32","unstructured":"Emerson EA, Jutla CS (1991) Tree automata, mu-calculus and determinacy. In: FOCS. IEEE, pp 368\u2013377"},{"key":"2658_CR33","doi-asserted-by":"crossref","unstructured":"Fagin R, Halpern JY, Moses Y, M. Y. Vardi. (1995) Reasoning about Knowledge. The MIT press, Cambridge","DOI":"10.7551\/mitpress\/5803.001.0001"},{"key":"2658_CR34","doi-asserted-by":"crossref","unstructured":"Filiot E, Gentilini R, Raskin J-F (2018) Rational synthesis under imperfect information. In: Proceedings of the 33rd Annual ACM\/IEEE Symposium on Logic in Computer Science. ACM","DOI":"10.1145\/3209108.3209164"},{"key":"2658_CR35","doi-asserted-by":"crossref","unstructured":"Finus M, Rundshagen B (2003) A non-cooperative foundation of core-stability in positive externality ntu-coalition games. Nota Di Lavoro 31.2003 Economics Energy Environment","DOI":"10.2139\/ssrn.406400"},{"key":"2658_CR36","doi-asserted-by":"crossref","unstructured":"Fisman D, Kupferman O, Lustig Y (2010) Rational synthesis. In: TACAS, volume 6015 of LNCS. Springer, pp 190\u2013204","DOI":"10.1007\/978-3-642-12002-2_16"},{"key":"2658_CR37","unstructured":"Gao T, Gutierrez J, Wooldridge M (2017) Iterated boolean games for rational verification. In: Larson K, Winikoff M, Das S, Durfee EH (eds) Proceedings of the 16th Conference on Autonomous Agents and MultiAgent Systems, AAMAS. ACM, Sa\u0307o Paulo, pp 705\u2013713"},{"key":"2658_CR38","doi-asserted-by":"crossref","unstructured":"Gutierrez J, Hammond L, Lin A, Najib M, Wooldridge M (2021) Rational verification for probabilistic systems. In: Proceedings of the 18th International Conference on Principles of Knowledge Representation and Reasoning (KR-21), Virtual. Forthcoming","DOI":"10.24963\/kr.2021\/30"},{"key":"2658_CR39","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1016\/j.ic.2015.03.011","volume":"242","author":"J Gutierrez","year":"2015","unstructured":"Gutierrez J, Harrenstein P, Wooldridge M (2015) Iterated boolean games. Inf Comput 242:53\u201379","journal-title":"Inf Comput"},{"key":"2658_CR40","unstructured":"Gutierrez J, Harrenstein P, Perelli G, Wooldridge M (2019) Nash equilibrium and bisimulation invariance. Log. Methods Comput. Sci. 15(3)"},{"key":"2658_CR41","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1016\/j.artint.2017.04.003","volume":"248","author":"J Gutierrez","year":"2017","unstructured":"Gutierrez J, Harrenstein P, Wooldridge M (2017) From model checking to equilibrium checking: Reactive modules for rational verification. Artif Intell 248:123\u2013157","journal-title":"Artif Intell"},{"key":"2658_CR42","unstructured":"Gutierrez J, Kraus S, Wooldridge M (2019) Cooperative concurrent games. In: Elkind E, Veloso M, Agmon N, Taylor ME (eds) Proceedings of the 18th International Conference on Autonomous Agents and MultiAgent Systems, AAMAS \u201919. International Foundation for Autonomous Agents and Multiagent Systems, Montreal, pp 1198\u20131206"},{"key":"2658_CR43","doi-asserted-by":"crossref","unstructured":"Gutierrez J, Murano A, Perelli G, Rubin S, Steeples T, Wooldridge M (2020) Equilibria for games with combined qualitative and quantitative objectives. Acta Informatica. Springer, pp 1\u201326","DOI":"10.1007\/s00236-020-00385-4"},{"key":"2658_CR44","doi-asserted-by":"crossref","unstructured":"Gutierrez J, Murano A, Perelli G, Rubin S, Wooldridge M (2017) Nash equilibria in concurrent games with lexicographic preferences. Association for the Advancement of Artificial Intelligence","DOI":"10.24963\/ijcai.2017\/148"},{"key":"2658_CR45","doi-asserted-by":"crossref","unstructured":"Gutierrez J, Najib M, Perelli G, Wooldridge M (2018) Eve: A tool for temporal equilibrium analysis. In: ATVA, Vol 11138 of LNCS. Springer, Cham, pp 551\u2013557","DOI":"10.1007\/978-3-030-01090-4_35"},{"key":"2658_CR46","doi-asserted-by":"publisher","unstructured":"Gutierrez J, Najib M, Perelli G, Wooldridge M (2019) On computational tractability for rational verification. In: Proceedings of the Twenty-Eighth International Joint Conference on Artificial Intelligence, IJCAI-19, pp 329\u2013335, DOI https:\/\/doi.org\/10.24963\/ijcai.2019\/47, (to appear in print)","DOI":"10.24963\/ijcai.2019\/47"},{"key":"2658_CR47","doi-asserted-by":"publisher","first-page":"103353","DOI":"10.1016\/j.artint.2020.103353","volume":"287","author":"J Gutierrez","year":"2020","unstructured":"Gutierrez J, Najib M, Perelli G, Wooldridge M (2020) Automated temporal equilibrium analysis: Verification and synthesis of multi-player games. Artif Intell 287:103353","journal-title":"Artif Intell"},{"key":"2658_CR48","doi-asserted-by":"crossref","unstructured":"Gutierrez J, Perelli G, Wooldridge M (2016) Imperfect information in reactive modules games. Inf Comput 261:650\u2013675. 2018 4th International Workshop on Strategic Reasoning (SR","DOI":"10.1016\/j.ic.2018.02.023"},{"key":"2658_CR49","unstructured":"Hammond L, Abate A, Gutierrez J, Wooldridge M (2021) Multi-agent reinforcement learning with temporal logic specifications. In: Proceedings of the 20th International Conference on Autonomous Agents and MultiAgent Systems, AAMAS \u201921. International Foundation for Autonomous Agents and Multiagent Systems. Forthcoming"},{"key":"2658_CR50","unstructured":"Hasanbeig M, Abate A, Kroening D (2018) Logically-constrained reinforcement learning. arXiv:1801.08099"},{"issue":"3","key":"2658_CR51","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1016\/S0020-0190(98)00150-1","volume":"68","author":"M Jurdzinski","year":"1998","unstructured":"Jurdzinski M (1998) Deciding the winner in parity games is in UP \u2229 co-up. Inf Process Lett 68(3):119\u2013124","journal-title":"Inf Process Lett"},{"key":"2658_CR52","doi-asserted-by":"crossref","unstructured":"Kupferman O (2018) Automata theory and model checking. In: Handbook of Model Checking. Springer International Publishing, pp 107\u2013151","DOI":"10.1007\/978-3-319-10575-8_4"},{"issue":"1","key":"2658_CR53","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/s10472-016-9508-8","volume":"78","author":"O Kupferman","year":"2016","unstructured":"Kupferman O, Perelli G, Vardi MY (2016) Synthesis with rational environments. Ann. Math. Artif Intell. 78(1):3\u201320","journal-title":"Ann. Math. Artif Intell."},{"key":"2658_CR54","doi-asserted-by":"crossref","unstructured":"Kwiatkowska M, Norman G, Parker D (2011) PRISM 4.0: Verification of probabilistic real-time systems. In: Gopalakrishnan G, Qadeer S (eds) Proceedings of 23rd International Conference on Computer Aided Verification (CAV\u201911), volume 6806 of LNCS. Springer, pp 585\u2013591","DOI":"10.1007\/978-3-642-22110-1_47"},{"key":"2658_CR55","doi-asserted-by":"crossref","unstructured":"Kwiatkowska M, Norman G, Parker D, Santos G (2018) Automated verification of concurrent stochastic games. In: Quantitative Evaluation of Systems. Springer International Publishing, pp 223\u2013239","DOI":"10.1007\/978-3-319-99154-2_14"},{"key":"2658_CR56","doi-asserted-by":"crossref","unstructured":"Kwiatkowska M, Norman G, Parker D, Santos Gl (2020) Automatic verification of concurrent stochastic systems. Formal Methods in System Design. To appear","DOI":"10.1007\/s10703-020-00356-y"},{"key":"2658_CR57","doi-asserted-by":"crossref","unstructured":"Kwiatkowska M, Norman G, Parker D, Santos G (2020) PRISM-games 3.0: Stochastic game verification with concurrency, equilibria and time. In: Computer Aided Verification. Springer International Publishing, pp 475\u2013487","DOI":"10.1007\/978-3-030-53291-8_25"},{"key":"2658_CR58","doi-asserted-by":"crossref","unstructured":"Lomuscio A, Raimondi F (2006) MCMAS: A tool for verifying multi-agent systems. In: Proceedings of The Twelfth International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS-2006). Springer, Berlin","DOI":"10.1007\/11691372_31"},{"issue":"1","key":"2658_CR59","doi-asserted-by":"publisher","first-page":"9","DOI":"10.1007\/s10009-015-0378-x","volume":"19","author":"A Lomuscio","year":"2017","unstructured":"Lomuscio A, Qu H, Raimondi F (2017) MCMAS: An open-source model checker for the verification of multi-agent systems. Int J Softw Tools Technol Transfer 19(1):9\u201330","journal-title":"Int J Softw Tools Technol Transfer"},{"key":"2658_CR60","doi-asserted-by":"crossref","unstructured":"Maler O, Nickovic D (2004) Monitoring temporal properties of continuous signals. In: Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems. Springer, Berlin, pp 152\u2013166","DOI":"10.1007\/978-3-540-30206-3_12"},{"key":"2658_CR61","doi-asserted-by":"crossref","unstructured":"Maschler M, Solan E, Zamir S (2013) Game Theory. Cambridge University Press. Cambridge","DOI":"10.1017\/CBO9780511794216"},{"issue":"4","key":"2658_CR62","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1145\/2631917","volume":"15","author":"F Mogavero","year":"2014","unstructured":"Mogavero F, Murano A, Perelli G, Vardi MY (2014) Reasoning about strategies: on the model-checking problem. ACM Trans Comput Logic 15(4):47. https:\/\/doi.org\/10.1145\/2631917","journal-title":"ACM Trans Comput Logic"},{"key":"2658_CR63","doi-asserted-by":"crossref","unstructured":"Nisan N, Roughgarden T, Tardos E, Vazirani VV (eds) (2007) Algorithmic Game Theory. Cambridge University Press, Cambridge","DOI":"10.1017\/CBO9780511800481"},{"key":"2658_CR64","unstructured":"Osborne MJ, Rubinstein A (1994) A course in game theory. The MIT press, Cambridge"},{"key":"2658_CR65","doi-asserted-by":"crossref","unstructured":"Piterman N (2007) From nondeterministic b\u00fcchi and streett automata to deterministic parity automata. Log Methods Comput Sci. 3(3)","DOI":"10.2168\/LMCS-3(3:5)2007"},{"key":"2658_CR66","doi-asserted-by":"crossref","unstructured":"Pnueli A (1977) The temporal logic of programs. In: Proceedings of the Eighteenth IEEE Symposium on the Foundations of Computer Science, pp 46\u201357","DOI":"10.1109\/SFCS.1977.32"},{"key":"2658_CR67","doi-asserted-by":"crossref","unstructured":"Pnueli A, Rosner R (1989) On the synthesis of an asynchronous reactive module. In: Proceedings of the Sixteenth International Colloquium on Automata, Languages, and Programs","DOI":"10.1007\/BFb0035790"},{"key":"2658_CR68","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1016\/j.artint.2012.03.007","volume":"186","author":"T Rahwan","year":"2012","unstructured":"Rahwan T, Michalak T, Wooldridge M, Jennings NR (2012) Anytime coalition structure generation in multi-agent systems with positive or negative externalities. Artif Intell 186:95\u2013 122","journal-title":"Artif Intell"},{"issue":"4","key":"2658_CR69","doi-asserted-by":"publisher","first-page":"1093","DOI":"10.1257\/00028280260344632","volume":"92","author":"A Roth","year":"2002","unstructured":"Roth A, Ockenfels A (2002) Last-minute bidding and the rules for ending second-price auctions: Evidence from eBay and Amazon auctions on the internet. Am Econ Rev 92(4):1093\u2013 1103","journal-title":"Am Econ Rev"},{"issue":"3","key":"2658_CR70","first-page":"387","volume":"3","author":"LM Ruane","year":"1990","unstructured":"Ruane LM (1990) Process synchronization in the UTS kernel. Comput Syst 3(3):387\u2013421","journal-title":"Comput Syst"},{"key":"2658_CR71","unstructured":"Ruys TC, Langerak R (1997) Validation of bosch\u2019 mobile communication network architecture with spin. In: Inproceedings of SPIN97, the Third International Workshop on SPIN. University of Twente"},{"issue":"1","key":"2658_CR72","doi-asserted-by":"publisher","first-page":"165","DOI":"10.1016\/S0004-3702(98)00045-9","volume":"101","author":"O Shehory","year":"1998","unstructured":"Shehory O, Kraus S (1998) Methods for task allocation via agent coalition formation. Artif Intell 101(1):165\u2013200","journal-title":"Artif Intell"},{"key":"2658_CR73","doi-asserted-by":"crossref","unstructured":"Shoham Y, Leyton-Brown K (2008) Multiagent systems algorithmic, Game-Theoretic, and logical foundations. Cambridge University Press, Cambridge","DOI":"10.1017\/CBO9780511811654"},{"issue":"3","key":"2658_CR74","doi-asserted-by":"publisher","first-page":"733","DOI":"10.1145\/3828.3837","volume":"32","author":"AP Sistla","year":"1985","unstructured":"Sistla AP, Clarke EM (1985) The complexity of propositional linear temporal logics. J ACM 32(3):733\u2013749","journal-title":"J ACM"},{"key":"2658_CR75","unstructured":"Strejcek J (2004) Linear temporal logic: Expressiveness and model checking. PhD thesis, PhD thesis, Faculty of Informatics Masaryk University in Brno"},{"key":"2658_CR76","doi-asserted-by":"crossref","unstructured":"Ummels M, Wojtczak D (2011) The Complexity of Nash Equilibria in Limit-Average games. CoRR, arXiv:1109.6220","DOI":"10.2168\/LMCS-7(3:20)2011"},{"key":"2658_CR77","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1016\/j.jet.2015.04.005","volume":"158","author":"M Uyan\u0131k","year":"2015","unstructured":"Uyan\u0131k M (2015) On the nonemptiness of the \u03b1-core of discontinuous games: Transferable and nontransferable utilities. J Econ Theory 158:213\u2013231","journal-title":"J Econ Theory"},{"key":"2658_CR78","doi-asserted-by":"crossref","unstructured":"van der Hoek W, Lomuscio A, Wooldridge M (2005) On the complexity of practical ATL model checking. In: Proceedings of the Fifth International Joint Conference on Autonomous Agents and Multiagent Systems (AAMAS-2006), Hakodate","DOI":"10.1145\/1160633.1160665"},{"key":"2658_CR79","doi-asserted-by":"crossref","unstructured":"Vardi MY (2001) Branching vs. linear time: Final showdown. In: Margaria T, Yi W (eds) Proceedings of the 2001 Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2001 (LNCS Volume 2031). Springer, Berlin, pp 1\u201322","DOI":"10.1007\/3-540-45319-9_1"},{"key":"2658_CR80","unstructured":"Vardi MY, Wolper P (1986) An automata-theoretic approach to automatic program verification. In: First Symposium in Logic in Computer Science (LICS)"},{"key":"2658_CR81","doi-asserted-by":"crossref","unstructured":"Winskel G (1986) Event structures. In: Advances in Petri Nets","DOI":"10.1007\/3-540-17906-2_31"},{"key":"2658_CR82","unstructured":"Wooldridge M (2009) An Introduction to Multiagent Systems, 2nd edn. Wiley"},{"key":"2658_CR83","doi-asserted-by":"crossref","unstructured":"Wooldridge M, Gutierrez J, Harrenstein P, Marchioni E, Perelli G, Toumi A (2016) Rational verification: From model checking to equilibrium checking. In: Schuurmans D, Wellman MP (eds) Proceedings of the Thirtieth AAAI Conference on Artificial Intelligence. AAAI Press, Phoenix, pp 4184\u20134191","DOI":"10.1609\/aaai.v30i1.9878"},{"issue":"2","key":"2658_CR84","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1006\/game.1997.0567","volume":"20","author":"S-S Yi","year":"1997","unstructured":"Yi S-S (1997) Stable coalition structures with externalities. Games Econ Behav 20(2):201\u2013237","journal-title":"Games Econ Behav"}],"container-title":["Applied Intelligence"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10489-021-02658-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10489-021-02658-y\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10489-021-02658-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T18:27:10Z","timestamp":1725560830000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10489-021-02658-y"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,8,3]]},"references-count":84,"journal-issue":{"issue":"9","published-print":{"date-parts":[[2021,9]]}},"alternative-id":["2658"],"URL":"https:\/\/doi.org\/10.1007\/s10489-021-02658-y","relation":{},"ISSN":["0924-669X","1573-7497"],"issn-type":[{"value":"0924-669X","type":"print"},{"value":"1573-7497","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,8,3]]},"assertion":[{"value":"30 June 2021","order":1,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"3 August 2021","order":2,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}