Abstract
Rational verification 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 CTL, and polynomial space with LTL specifications, rational verification is much harder: the key decision problems for rational verification are 2EXPTIME-complete with LTL 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 GR(1), a fragment of LTL 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’ goals given by mean-payoff utility functions—arguably 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 PSPACE-complete or NP-complete.
Article PDF
Similar content being viewed by others
Explore related subjects
Discover the latest articles, news and stories from top researchers in related subjects.Avoid common mistakes on your manuscript.
References
Alur, R., Henzinger, T., Kupferman, O.: Alternating-time temporal logic. J. ACM 49(5), 672–713 (2002)
Alur, R., La Torre, S.: Deterministic generators and games for LTL fragments. ACM Trans. Comput. Log. 5(1), 1–25 (2004)
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–424. Springer (2010)
Bloem, R., Jobstmann, B., Piterman, N., Pnueli, A., Sa’ar, Y.: Synthesis of reactive(1) designs. J. Comput. Syst. Sci. 78(3), 911–938 (2012)
Boker, U., Chatterjee, K., Henzinger, T., Kupferman, O.: Temporal specifications with accumulative values. ACM Trans. Comput. Logic 15 (4), 27:1–27:25 (2014). https://doi.org/10.1145/2629686
Calude, C., Jain, S., Khoussainov, B., Li, W., Stephan, F.: Deciding parity games in quasipolynomial time. In: STOC, pp. 252–263. ACM (2017)
Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press (2002)
Clarke, E.M., Grumberg, O., Kroening, D., Peled, D., Veith, H.: Model Checking, 2nd edn. MIT Press (2018)
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–121:15. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.ICALP.2016.121 (2016)
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–38:15. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.CONCUR.2018.38 (2018)
Emerson, E.: Temporal and modal logic. In: Handbook of Theoretical Computer Science Volume B: Formal Models and Semantics, pp. 996–1072. Elsevier (1990)
Filiot, E., Gentilini, R., Raskin, J.F.: Rational Synthesis Under Imperfect Information. In: LICS, pp. 422–431. ACM (2018)
Fisman, D., Kupferman, O., Lustig, Y.: Rational Synthesis. In: TACAS, LNCS, vol. 6015, pp. 190–204. Springer (2010)
Gao, T., Gutierrez, J., Wooldridge, M.: Iterated Boolean Games for Rational Verification. In: AAMAS, pp. 705–713. ACM (2017)
Gutierrez, J., Harrenstein, P., Wooldridge, M.: Expresiveness and Complexity Results for Strategic Reasoning. In: CONCUR, LIPIcs, vol. 42, pp. 268–282. Schloss Dagstuhl (2015)
Gutierrez, J., Harrenstein, P., Wooldridge, M.: Iterated Boolean Games. Inf. Comput. 242, 53–79 (2015)
Gutierrez, J., Harrenstein, P., Wooldridge, M.: From Model Checking to Equilibrium Checking: Reactive Modules for Rational Verification. Artif. Intell. 248, 123–157 (2017)
Gutierrez, J., Harrenstein, P., Wooldridge, M.: Reasoning about equilibria in game-like concurrent systems. Ann. Pure Appl. Logic 168(2), 373–403 (2017)
Gutierrez, J., Murano, A., Perelli, G., Rubin, S., Wooldridge, M.: Nash equilibria in concurrent games with lexicographic preferences. In: IJCAI, pp. 1067–1073. https://doi.org/10.24963/ijcai.2017/148 (2017)
Gutierrez, J., Najib, M., Perelli, G., Wooldridge, M.: EVE: A tool for temporal equilibrium analysis. In: ATVA, LNCS, vol. 11138, pp. 551–557. Springer (2018)
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
Gutierrez, J., Perelli, G., Wooldridge, M.: Imperfect information in reactive modules games. Inf. Comput. 261(Part), 650–675 (2018)
Kupferman, O.: Automata Theory and Model Checking Handbook of TCS (2015)
Kupferman, O., Perelli, G., Vardi, M.: Synthesis with rational environments. Ann. Math. Artif. Intell. 78(1), 3–20 (2016)
Osborne, M., Rubinstein, A.: A Course in Game Theory. MIT Press (1994)
Piterman, N., Pnueli, A.: Faster solutions of Rabin and Streett games. In: LICS, pp. 275–284. https://doi.org/10.1109/LICS.2006.23 (2006)
Pnueli, A.: The temporal logic of programs. In: FOCS, pp. 46–57. IEEE (1977)
Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: POPL, pp. 179–190. ACM Press (1989)
Rauch Henzinger, M., Telle, J.: Faster algorithms for the nonemptiness of streett automata and for communication protocol pruning. In: SWAT, pp. 16–27 (1996)
Sikorski, K: Bisection is optimal. Numer. Math. 40(1), 111–117 (1982)
Steeples, T., Gutierrez, J., Wooldridge, M.J.: Mean-payoff games with ω-regular specifications. In: Dignum, F., Lomuscio, A., Endriss, U., Nowé, A. (eds.) AAMAS ’21: 20th International Conference on Autonomous Agents and Multiagent Systems, Virtual Event, United Kingdom, May 3-7, 2021, pp. 1272–1280. ACM (2021)
Ummels, M., Wojtczak, D.: The Complexity of Nash Equilibria in Limit-Average Games. In: CONCUR, pp. 482–496 (2011). https://doi.org/10.1007/978-3-642-23217-6\_32
Wooldridge, M., Gutierrez, J., Harrenstein, P., Marchioni, E., Perelli, G., Toumi, A.: Rational verification: From model checking to equilibrium checking. In: AAAI, pp. 4184–4191. AAAI Press (2016)
Zwick, U., Paterson, M.: The complexity of mean payoff games on graphs. Theor. Comput. Sci. 158(1), 343–359 (1996). https://doi.org/10.1016/0304-3975(95)00188-3
Acknowledgements
Wooldridge gratefully acknowledges the support of the ERC under Advanced Grant 291528 (“RACE”), and the support of the Alan Turing Institute in London. Najib acknowledges the support of ERC Starting Grant 759969 (AV-SMP). Perelli acknowledges the support of the ERC project “WhiteMech” (grant agreement No 834228) and the EU ICT-48 2020 project TAILOR (No. 952215).
Funding
Open Access funding enabled and organized by CAUL and its Member Institutions
Author information
Authors and Affiliations
Corresponding author
Ethics declarations
Conflict of Interests
The authors declare that they have no conflict of interest.
Additional information
Publisher’s note
Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.
Rights and permissions
Open Access This article is licensed under a Creative Commons Attribution 4.0 International License, which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons licence, and indicate if changes were made. The images or other third party material in this article are included in the article's Creative Commons licence, unless indicated otherwise in a credit line to the material. If material is not included in the article's Creative Commons licence and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder. To view a copy of this licence, visit http://creativecommons.org/licenses/by/4.0/.
About this article
Cite this article
Gutierrez, J., Najib, M., Perelli, G. et al. On the complexity of rational verification. Ann Math Artif Intell 91, 409–430 (2023). https://doi.org/10.1007/s10472-022-09804-3
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s10472-022-09804-3