{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,24]],"date-time":"2025-09-24T10:23:51Z","timestamp":1758709431645,"version":"3.37.3"},"reference-count":34,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2022,7,14]],"date-time":"2022-07-14T00:00:00Z","timestamp":1657756800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2022,7,14]],"date-time":"2022-07-14T00:00:00Z","timestamp":1657756800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/100010663","name":"H2020 European Research Council","doi-asserted-by":"publisher","award":["291528"],"award-info":[{"award-number":["291528"]}],"id":[{"id":"10.13039\/100010663","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100010663","name":"H2020 European Research Council","doi-asserted-by":"publisher","award":["834228"],"award-info":[{"award-number":["834228"]}],"id":[{"id":"10.13039\/100010663","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100010661","name":"Horizon 2020 Framework Programme","doi-asserted-by":"publisher","award":["952215"],"award-info":[{"award-number":["952215"]}],"id":[{"id":"10.13039\/100010661","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001779","name":"Monash University","doi-asserted-by":"crossref","id":[{"id":"10.13039\/501100001779","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Ann Math Artif Intell"],"published-print":{"date-parts":[[2023,8]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p><jats:italic>Rational verification<\/jats:italic> refers to the problem of checking which temporal logic properties hold of a concurrent\/multiagent system, under the assumption that agents in the system choose strategies that form a game theoretic equilibrium. Rational verification can be understood as a counterpart to model checking for multiagent systems, but while classical model checking can be done in polynomial time for some temporal logic specification languages such as , and polynomial space with  specifications, rational verification is much harder: the key decision problems for rational verification are 2-complete with  specifications, even when using explicit-state system representations. Against this background, our contributions in this paper are threefold. First, we show that the complexity of rational verification can be greatly reduced by restricting specifications to , a fragment of  that can represent a broad and practically useful class of response properties of reactive systems. In particular, we show that for a number of relevant settings, rational verification can be done in polynomial space and even in polynomial time. Second, we provide improved complexity results for rational verification when considering players\u2019 goals given by <jats:italic>mean-payoff<\/jats:italic> utility functions\u2014arguably the most widely used approach for quantitative objectives in concurrent and multiagent systems. Finally, we consider the problem of computing outcomes that satisfy social welfare constraints. To this end, we consider both utilitarian and egalitarian social welfare and show that computing such outcomes is either -complete or -complete.<\/jats:p>","DOI":"10.1007\/s10472-022-09804-3","type":"journal-article","created":{"date-parts":[[2022,7,14]],"date-time":"2022-07-14T15:04:59Z","timestamp":1657811099000},"page":"409-430","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["On the complexity of rational verification"],"prefix":"10.1007","volume":"91","author":[{"given":"Julian","family":"Gutierrez","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Muhammad","family":"Najib","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8687-6323","authenticated-orcid":false,"given":"Giuseppe","family":"Perelli","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Michael","family":"Wooldridge","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2022,7,14]]},"reference":[{"issue":"5","key":"9804_CR1","doi-asserted-by":"publisher","first-page":"672","DOI":"10.1145\/585265.585270","volume":"49","author":"R Alur","year":"2002","unstructured":"Alur, R., Henzinger, T., Kupferman, O.: Alternating-time temporal logic. J. ACM 49(5), 672\u2013713 (2002)","journal-title":"J. ACM"},{"issue":"1","key":"9804_CR2","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/963927.963928","volume":"5","author":"R Alur","year":"2004","unstructured":"Alur, R., La Torre, S.: Deterministic generators and games for LTL fragments. ACM Trans. Comput. Log. 5(1), 1\u201325 (2004)","journal-title":"ACM Trans. Comput. Log."},{"doi-asserted-by":"crossref","unstructured":"Bloem, R., Chatterjee, K., Greimel, K., Henzinger, T.A., Jobstmann, B.: Robustness in the presence of liveness. In: Touili, T., Cook, B., Jackson, P.B. (eds.) Computer Aided Verification, 22nd International Conference, CAV 2010, Edinburgh, UK, July 15-19, 2010. Proceedings, Lecture Notes in Computer Science, vol. 6174, pp. 410\u2013424. Springer (2010)","key":"9804_CR3","DOI":"10.1007\/978-3-642-14295-6_36"},{"issue":"3","key":"9804_CR4","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.: Synthesis of reactive(1) designs. J. Comput. Syst. Sci. 78(3), 911\u2013938 (2012)","journal-title":"J. Comput. Syst. Sci."},{"issue":"4","key":"9804_CR5","doi-asserted-by":"publisher","first-page":"27:1","DOI":"10.1145\/2629686","volume":"15","author":"U Boker","year":"2014","unstructured":"Boker, U., Chatterjee, K., Henzinger, T., Kupferman, O.: Temporal specifications with accumulative values. ACM Trans. Comput. Logic 15 (4), 27:1\u201327:25 (2014). https:\/\/doi.org\/10.1145\/2629686","journal-title":"ACM Trans. Comput. Logic"},{"doi-asserted-by":"crossref","unstructured":"Calude, C., Jain, S., Khoussainov, B., Li, W., Stephan, F.: Deciding parity games in quasipolynomial time. In: STOC, pp. 252\u2013263. ACM (2017)","key":"9804_CR6","DOI":"10.1145\/3055399.3055409"},{"unstructured":"Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press (2002)","key":"9804_CR7"},{"unstructured":"Clarke, E.M., Grumberg, O., Kroening, D., Peled, D., Veith, H.: Model Checking, 2nd edn. MIT Press (2018)","key":"9804_CR8"},{"doi-asserted-by":"publisher","unstructured":"Condurache, R., Filiot, E., Gentilini, R., Raskin, J.: The complexity of rational synthesis. In: Chatzigiannakis, I., Mitzenmacher, M., Rabani, Y., Sangiorgi, D. (eds.) 43rd International Colloquium on Automata, Languages, and Programming, ICALP 2016, July 11-15, 2016, Rome, Italy, LIPIcs, vol. 55, pp. 121:1\u2013121:15. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik. https:\/\/doi.org\/10.4230\/LIPIcs.ICALP.2016.121 (2016)","key":"9804_CR9","DOI":"10.4230\/LIPIcs.ICALP.2016.121"},{"doi-asserted-by":"publisher","unstructured":"Condurache, R., Oualhadj, Y., Troquard, N.: The complexity of rational synthesis for concurrent games. In: Schewe, S., Zhang, L. (eds.) 29th International Conference on Concurrency Theory, CONCUR 2018, September 4-7, 2018, Beijing, China, LIPIcs, vol. 118, pp. 38:1\u201338:15. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik. https:\/\/doi.org\/10.4230\/LIPIcs.CONCUR.2018.38 (2018)","key":"9804_CR10","DOI":"10.4230\/LIPIcs.CONCUR.2018.38"},{"doi-asserted-by":"crossref","unstructured":"Emerson, E.: Temporal and modal logic. In: Handbook of Theoretical Computer Science Volume B: Formal Models and Semantics, pp. 996\u20131072. Elsevier (1990)","key":"9804_CR11","DOI":"10.1016\/B978-0-444-88074-1.50021-4"},{"doi-asserted-by":"crossref","unstructured":"Filiot, E., Gentilini, R., Raskin, J.F.: Rational Synthesis Under Imperfect Information. In: LICS, pp. 422\u2013431. ACM (2018)","key":"9804_CR12","DOI":"10.1145\/3209108.3209164"},{"doi-asserted-by":"crossref","unstructured":"Fisman, D., Kupferman, O., Lustig, Y.: Rational Synthesis. In: TACAS, LNCS, vol. 6015, pp. 190\u2013204. Springer (2010)","key":"9804_CR13","DOI":"10.1007\/978-3-642-12002-2_16"},{"unstructured":"Gao, T., Gutierrez, J., Wooldridge, M.: Iterated Boolean Games for Rational Verification. In: AAMAS, pp. 705\u2013713. ACM (2017)","key":"9804_CR14"},{"unstructured":"Gutierrez, J., Harrenstein, P., Wooldridge, M.: Expresiveness and Complexity Results for Strategic Reasoning. In: CONCUR, LIPIcs, vol. 42, pp. 268\u2013282. Schloss Dagstuhl (2015)","key":"9804_CR15"},{"key":"9804_CR16","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.: Iterated Boolean Games. Inf. Comput. 242, 53\u201379 (2015)","journal-title":"Inf. Comput."},{"key":"9804_CR17","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.: From Model Checking to Equilibrium Checking: Reactive Modules for Rational Verification. Artif. Intell. 248, 123\u2013157 (2017)","journal-title":"Artif. Intell."},{"issue":"2","key":"9804_CR18","doi-asserted-by":"publisher","first-page":"373","DOI":"10.1016\/j.apal.2016.10.009","volume":"168","author":"J Gutierrez","year":"2017","unstructured":"Gutierrez, J., Harrenstein, P., Wooldridge, M.: Reasoning about equilibria in game-like concurrent systems. Ann. Pure Appl. Logic 168(2), 373\u2013403 (2017)","journal-title":"Ann. Pure Appl. Logic"},{"doi-asserted-by":"publisher","unstructured":"Gutierrez, J., Murano, A., Perelli, G., Rubin, S., Wooldridge, M.: Nash equilibria in concurrent games with lexicographic preferences. In: IJCAI, pp. 1067\u20131073. https:\/\/doi.org\/10.24963\/ijcai.2017\/148 (2017)","key":"9804_CR19","DOI":"10.24963\/ijcai.2017\/148"},{"doi-asserted-by":"crossref","unstructured":"Gutierrez, J., Najib, M., Perelli, G., Wooldridge, M.: EVE: A tool for temporal equilibrium analysis. In: ATVA, LNCS, vol. 11138, pp. 551\u2013557. Springer (2018)","key":"9804_CR20","DOI":"10.1007\/978-3-030-01090-4_35"},{"key":"9804_CR21","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.J.: Automated temporal equilibrium analysis: Verification and synthesis of multi-player games. Artif. Intell. 287, 103353 (2020). https:\/\/doi.org\/10.1016\/j.artint.2020.103353","journal-title":"Artif. Intell."},{"issue":"Part","key":"9804_CR22","doi-asserted-by":"publisher","first-page":"650","DOI":"10.1016\/j.ic.2018.02.023","volume":"261","author":"J Gutierrez","year":"2018","unstructured":"Gutierrez, J., Perelli, G., Wooldridge, M.: Imperfect information in reactive modules games. Inf. Comput. 261(Part), 650\u2013675 (2018)","journal-title":"Inf. Comput."},{"unstructured":"Kupferman, O.: Automata Theory and Model Checking Handbook of TCS (2015)","key":"9804_CR23"},{"issue":"1","key":"9804_CR24","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, M.: Synthesis with rational environments. Ann. Math. Artif. Intell. 78(1), 3\u201320 (2016)","journal-title":"Ann. Math. Artif. Intell."},{"unstructured":"Osborne, M., Rubinstein, A.: A Course in Game Theory. MIT Press (1994)","key":"9804_CR25"},{"doi-asserted-by":"publisher","unstructured":"Piterman, N., Pnueli, A.: Faster solutions of Rabin and Streett games. In: LICS, pp. 275\u2013284. https:\/\/doi.org\/10.1109\/LICS.2006.23 (2006)","key":"9804_CR26","DOI":"10.1109\/LICS.2006.23"},{"doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: FOCS, pp. 46\u201357. IEEE (1977)","key":"9804_CR27","DOI":"10.1109\/SFCS.1977.32"},{"doi-asserted-by":"crossref","unstructured":"Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: POPL, pp. 179\u2013190. ACM Press (1989)","key":"9804_CR28","DOI":"10.1145\/75277.75293"},{"doi-asserted-by":"crossref","unstructured":"Rauch Henzinger, M., Telle, J.: Faster algorithms for the nonemptiness of streett automata and for communication protocol pruning. In: SWAT, pp. 16\u201327 (1996)","key":"9804_CR29","DOI":"10.1007\/3-540-61422-2_117"},{"issue":"1","key":"9804_CR30","doi-asserted-by":"publisher","first-page":"111","DOI":"10.1007\/BF01459080","volume":"40","author":"K Sikorski","year":"1982","unstructured":"Sikorski, K: Bisection is optimal. Numer. Math. 40(1), 111\u2013117 (1982)","journal-title":"Numer. Math."},{"unstructured":"Steeples, T., Gutierrez, J., Wooldridge, M.J.: Mean-payoff games with \u03c9-regular specifications. In: Dignum, F., Lomuscio, A., Endriss, U., Now\u00e9, A. (eds.) AAMAS \u201921: 20th International Conference on Autonomous Agents and Multiagent Systems, Virtual Event, United Kingdom, May 3-7, 2021, pp. 1272\u20131280. ACM (2021)","key":"9804_CR31"},{"doi-asserted-by":"publisher","unstructured":"Ummels, M., Wojtczak, D.: The Complexity of Nash Equilibria in Limit-Average Games. In: CONCUR, pp. 482\u2013496 (2011). https:\/\/doi.org\/10.1007\/978-3-642-23217-6\\_32","key":"9804_CR32","DOI":"10.1007\/978-3-642-23217-6\\_32"},{"doi-asserted-by":"crossref","unstructured":"Wooldridge, M., Gutierrez, J., Harrenstein, P., Marchioni, E., Perelli, G., Toumi, A.: Rational verification: From model checking to equilibrium checking. In: AAAI, pp. 4184\u20134191. AAAI Press (2016)","key":"9804_CR33","DOI":"10.1609\/aaai.v30i1.9878"},{"issue":"1","key":"9804_CR34","doi-asserted-by":"publisher","first-page":"343","DOI":"10.1016\/0304-3975(95)00188-3","volume":"158","author":"U Zwick","year":"1996","unstructured":"Zwick, U., Paterson, M.: The complexity of mean payoff games on graphs. Theor. Comput. Sci. 158(1), 343\u2013359 (1996). https:\/\/doi.org\/10.1016\/0304-3975(95)00188-3","journal-title":"Theor. Comput. Sci."}],"container-title":["Annals of Mathematics and Artificial Intelligence"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10472-022-09804-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10472-022-09804-3\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10472-022-09804-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,8,11]],"date-time":"2023-08-11T07:15:14Z","timestamp":1691738114000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10472-022-09804-3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,7,14]]},"references-count":34,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2023,8]]}},"alternative-id":["9804"],"URL":"https:\/\/doi.org\/10.1007\/s10472-022-09804-3","relation":{},"ISSN":["1012-2443","1573-7470"],"issn-type":[{"type":"print","value":"1012-2443"},{"type":"electronic","value":"1573-7470"}],"subject":[],"published":{"date-parts":[[2022,7,14]]},"assertion":[{"value":"23 June 2022","order":1,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"14 July 2022","order":2,"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 that they have no conflict of interest.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"<!--Emphasis Type='Bold' removed-->Conflict of Interests"}}]}}