×

zbMATH — the first resource for mathematics

Automated temporal equilibrium analysis: verification and synthesis of multi-player games. (English) Zbl 07274584
Summary: In the context of multi-agent systems, the rational verification problem is concerned with checking which temporal logic properties will hold in a system when its constituent agents are assumed to behave rationally and strategically in pursuit of individual objectives. Typically, those objectives are expressed as temporal logic formulae which the relevant agent desires to see satisfied. Unfortunately, rational verification is computationally complex, and requires specialised techniques in order to obtain practically useable implementations. In this paper, we present such a technique. This technique relies on a reduction of the rational verification problem to the solution of a collection of parity games. Our approach has been implemented in the Equilibrium Verification Environment (EVE) system. The EVE system takes as input a model of a concurrent/multi-agent system represented using the Simple Reactive Modules Language (SRML), where agent goals are represented as Linear Temporal Logic (LTL) formulae, together with a claim about the equilibrium behaviour of the system, also expressed as an LTL formula. EVE can then check whether the claim holds on some (or every) computation of the system that could arise through agents choosing Nash equilibrium strategies; it can also check whether a system has a Nash equilibrium, and synthesise individual strategies for players in the multi-player game. After presenting our basic framework, we describe our new technique and prove its correctness. We then describe our implementation in the EVE system, and present experimental results which show that EVE performs favourably in comparison to other existing tools that support rational verification.
MSC:
68T Artificial intelligence
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Clarke, E. M.; Grumberg, O.; Peled, D. A., Model Checking (2002), MIT Press: MIT Press Cambridge, MA, USA
[2] Wooldridge, M., Introduction to Multiagent Systems (2001), Wiley: Wiley Chichester, UK
[3] Shoham, Y.; Leyton-Brown, K., Multiagent Systems: Algorithmic, Game-Theoretic, and Logical Foundations (2008), CUP · Zbl 1163.91006
[4] Osborne, M. J.; Rubinstein, A., A Course in Game Theory (1994), MIT Press · Zbl 1194.91003
[5] Halpern, J. Y., Beyond Nash equilibrium: solution concepts for the 21st century, (KR (2008), AAAI Press), 6-15 · Zbl 1301.91008
[6] Abraham, I.; Alvisi, L.; Halpern, J. Y., Distributed computing meets game theory: combining insights from two fields, SIGACT News, 42, 2, 69-76 (2011)
[7] Gutierrez, J.; Harrenstein, P.; Wooldridge, M., From model checking to equilibrium checking: reactive modules for rational verification, Artif. Intell., 248, 123-157 (2017) · Zbl 1420.68129
[8] Wooldridge, M.; Gutierrez, J.; Harrenstein, P.; Marchioni, E.; Perelli, G.; Toumi, A., Rational verification: from model checking to equilibrium checking, (AAAI (2016)), 4184-4191
[9] EVE: a tool for temporal equilibrium analysis (2019)
[10] van der Hoek, W.; Lomuscio, A.; Wooldridge, M., On the complexity of practical ATL model checking, (AAMAS (2006), ACM), 201-208
[11] Pnueli, A., The temporal logic of programs, (FOCS (1977), IEEE), 46-57
[12] 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-34:47 (2014) · Zbl 1354.68178
[13] Gutierrez, J.; Harrenstein, P.; Wooldridge, M., Reasoning about equilibria in game-like concurrent systems, Ann. Pure Appl. Log., 168, 2, 373-403 (2017) · Zbl 1400.03057
[14] Fisman, D.; Kupferman, O.; Lustig, Y., Rational synthesis, (TACAS. TACAS, LNCS, vol. 6015 (2010), Springer), 190-204 · Zbl 1284.68396
[15] Gutierrez, J.; Harrenstein, P.; Wooldridge, M., Iterated Boolean games, Inf. Comput., 242, 53-79 (2015) · Zbl 1318.91012
[16] Chatterjee, K.; Henzinger, T. A.; Piterman, N., Strategy logic, Inf. Comput., 208, 6, 677-693 (2010) · Zbl 1205.68197
[17] Gutierrez, J.; Perelli, G.; Wooldridge, M., Imperfect information in reactive modules games, Inf. Comput., 261, Part, 650-675 (2018) · Zbl 1395.68188
[18] Löding, C., Basics on tree automata, (Modern Applications of Automata Theory (2012), Indian Institute of Science: Indian Institute of Science Bangalore, India), 79-110 · Zbl 1256.68103
[19] Emerson, E. A.; Jutla, C. S., Tree automata, mu-calculus and determinacy, (FOCS, IEEE (1991)), 368-377
[20] Jurdzinski, M., Deciding the winner in parity games is in UP ∩ co-up, Inf. Process. Lett., 68, 3, 119-124 (1998) · Zbl 1338.68109
[21] Calude, C. S.; Jain, S.; Khoussainov, B.; Li, W.; Stephan, F., Deciding parity games in quasipolynomial time, (STOC (2017), ACM), 252-263 · Zbl 1369.68234
[22] Kupferman, O., Automata theory and model checking, (Handbook of Model Checking (2018), Springer International Publishing), 107-151 · Zbl 1392.68255
[23] Gutierrez, J.; Najib, M.; Perelli, G.; Wooldridge, M., Eve: a tool for temporal equilibrium analysis, (ATVA. ATVA, LNCS, vol. 11138 (2018), Springer: Springer Cham), 551-557
[24] Alur, R.; Henzinger, T. A., Reactive modules, Form. Methods Syst. Des., 15, 1, 7-48 (1999)
[25] Alur, R.; Henzinger, T. A.; Mang, F. Y.C.; Qadeer, S.; Rajamani, S. K.; Tasiran, S., MOCHA: modularity in model checking, (CAV. CAV, LNCS, vol. 1427 (1998), Springer), 521-525
[26] Kwiatkowska, M. Z.; Norman, G.; Parker, D., PRISM: probabilistic model checking for performance and reliability analysis, ACM SIGMETRICS Perform. Eval. Rev., 36, 4, 40-45 (2009)
[27] Brafman, R. I.; Domshlak, C., From one to many: planning for loosely coupled multi-agent systems, (Proceedings of the Eighteenth International Conference on Automated Planning and Scheduling. Proceedings of the Eighteenth International Conference on Automated Planning and Scheduling, ICAPS 2008, Sydney, Australia, September 14-18, 2008 (2008)), 28-35
[28] Gutierrez, J.; Harrenstein, P.; Perelli, G.; Wooldridge, M., Nash equilibrium and bisimulation invariance, (CONCUR. CONCUR, Schloss Dagstuhl. CONCUR. CONCUR, Schloss Dagstuhl, LIPIcs, vol. 85 (2017)), 17:1-17:16 · Zbl 1442.68143
[29] Gutierrez, J.; Harrenstein, P.; Perelli, G.; Wooldridge, M. J., Nash equilibrium and bisimulation invariance, Log. Methods Comput. Sci., 15, 3 (2019) · Zbl 1442.68142
[30] Milner, R., Communication and Concurrency (1989), Prentice Hall · Zbl 0683.68008
[31] Hennessy, M.; Milner, R., Algebraic laws for nondeterminism and concurrency, J. ACM, 32, 1, 137-161 (1985) · Zbl 0629.68021
[32] Sistla, A. P.; Vardi, M. Y.; Wolper, P., The complementation problem for Büchi automata with applications to temporal logic, Theor. Comput. Sci., 49, 217-237 (1987) · Zbl 0613.03015
[33] Piterman, N., From nondeterministic Büchi and Streett automata to deterministic parity automata, Log. Methods Comput. Sci., 3, 3, 1-21 (2007) · Zbl 1125.68067
[34] Gutierrez, J.; Harrenstein, P.; Wooldridge, M., Expresiveness and complexity results for strategic reasoning, (CONCUR. CONCUR, Schloss Dagstuhl. CONCUR. CONCUR, Schloss Dagstuhl, LIPIcs, vol. 42 (2015)), 268-282 · Zbl 1374.68332
[35] Perrin, D.; Pin, J., Infinite Words, Pure and Applied Mathematics (2004), Elsevier
[36] Bouyer, P.; Brenguier, R.; Markey, N.; Ummels, M., Pure Nash equilibria in concurrent deterministic games, Log. Methods Comput. Sci., 11, 2, 1-72 (2015) · Zbl 1320.91010
[37] Zielonka, W., Infinite games on finitely coloured graphs with applications to automata on infinite trees, Theor. Comput. Sci., 200, 1-2, 135-183 (1998) · Zbl 0915.68120
[38] Gao, T.; Gutierrez, J.; Wooldridge, M., Iterated Boolean games for rational verification, (AAMAS (2017), ACM), 705-713
[39] Brenguier, R., PRALINE: a tool for computing Nash equilibria in concurrent games, (CAV. CAV, LNCS, vol. 8044 (2013), Springer), 890-895
[40] Cermák, P.; Lomuscio, A.; Mogavero, F.; Murano, A., MCMAS-SLK: a model checker for the verification of strategy logic specifications, (CAV. CAV, LNCS, vol. 8559 (2014), Springer), 525-532
[41] Cermák, P.; Lomuscio, A.; Mogavero, F.; Murano, A., Practical verification of multi-agent systems against SLK specifications, Inf. Comput., 261, Part, 588-614 (2018) · Zbl 1395.68255
[42] Lomuscio, A.; Qu, H.; Raimondi, F., MCMAS: an open-source model checker for the verification of multi-agent systems, Int. J. Softw. Tools Technol. Transf., 19, 1, 9-30 (2017)
[43] Gastin, P.; Oddoux, D., Fast LTL to Büchi automata translation, (CAV (2001), Springer), 53-65 · Zbl 0991.68044
[44] (2019), LTL 2 BA: fast translation from LTL formulae to Büchi automata
[45] Friedmann, O.; Lange, M., The PGsolver Collection of Parity Game Solvers - Version 3 (2010)
[46] (2019), PGSolver
[47] Alur, R.; Henzinger, T. A.; Kupferman, O., Alternating-time temporal logic, J. ACM, 49, 5, 672-713 (2002) · Zbl 1326.68181
[48] Ladin, R.; Liskov, B.; Shrira, L.; Ghemawat, S., Providing high availability using lazy replication, ACM Trans. Comput. Syst., 10, 4, 360-391 (1992)
[49] Fischer, M. J.; Michael, A., Sacrificing serializability to attain high availability of data in an unreliable network, (PODS (1982), ACM: ACM New York, NY, USA), 70-75
[50] Wuu, G. T.; Bernstein, A. J., Efficient solutions to the replicated log and dictionary problems, (PODC (1984), ACM: ACM New York, NY, USA), 233-242
[51] Gifford, D. K., Weighted voting for replicated data, (SOSP (1979), ACM: ACM New York, NY, USA), 150-162
[52] Gutierrez, J.; Najib, M.; Perelli, G.; Wooldridge, M. J., On computational tractability for rational verification, (IJCAI (2019)), 329-335, ijcai.org
[53] Emerson, E. A., Temporal and modal logic, (Handbook of Theoretical Computer Science, Volume B: Formal Models and Semantics (B) (1990), MIT Press: MIT Press Cambridge, MA, USA), 995-1072 · Zbl 0900.03030
[54] Kupferman, O.; Perelli, G.; Vardi, M. Y., Synthesis with rational environments, Ann. Math. Artif. Intell., 78, 1, 3-20 (2016) · Zbl 1372.68173
[55] Finkbeiner, B.; Schewe, S., Coordination logic, (CSL. CSL, LNCS, vol. 6247 (2010), Springer), 305-319 · Zbl 1287.03070
[56] Laroussinie, F.; Markey, N., Augmenting ATL with strategy contexts, Inf. Comput., 245, 98-123 (2015) · Zbl 1332.68140
[57] Cermák, P.; Lomuscio, A.; Murano, A., Verifying and synthesising multi-agent systems against one-goal strategy logic specifications, (AAAI (2015), AAAI Press), 2038-2044
[58] Cermák, P.; Lomuscio, A.; Mogavero, F.; Murano, A., Practical verification of multi-agent systems against SLK specifications, Inf. Comput., 261, Part, 588-614 (2018) · Zbl 1395.68255
[59] Kwiatkowska, M.; Parker, D.; Wiltsche, C., Prism-games 2.0: a tool for multi-objective strategy synthesis for stochastic games, (TACAS. TACAS, LNCS, vol. 9636 (2016), Springer), 560-566
[60] Toumi, A.; Gutierrez, J.; Wooldridge, M., A tool for the automated verification of Nash equilibria in concurrent games, (ICTAC. ICTAC, LNCS, vol. 9399 (2015), Springer), 583-594 · Zbl 06545749
[61] David, A.; Larsen, K. G.; Legay, A.; Mikucionis, M.; Poulsen, D. B., Uppaal SMC tutorial, Int. J. Softw. Tools Technol. Transf., 17, 4, 397-415 (2015)
[62] Kwiatkowska, M.; Norman, G.; Parker, D.; Santos, G., Equilibria-based probabilistic model checking for concurrent stochastic games, (FM. FM, LNCS, vol. 11800 (2019), Springer), 298-315
[63] David, A.; Jensen, P. G.; Larsen, K. G.; Mikucionis, M.; Taankvist, J. H., Uppaal stratego, (TACAS. TACAS, LNCS, vol. 9035 (2015), Springer), 206-211
[64] Bulychev, P. E.; David, A.; Larsen, K. G.; Legay, A.; Mikucionis, M., Computing Nash equilibrium in wireless ad hoc networks: a simulation-based approach, (Proceedings Second International Workshop on Interactions, Games and Protocols. Proceedings Second International Workshop on Interactions, Games and Protocols, IWIGP. Proceedings Second International Workshop on Interactions, Games and Protocols. Proceedings Second International Workshop on Interactions, Games and Protocols, IWIGP, EPTCS, vol. 78 (2012)), 1-14
[65] Milner, R., A Calculus of Communicating Systems, LNCS, vol. 92 (1980), Springer · Zbl 0452.68027
[66] De Nicola, R.; Vaandrager, F. W., Three logics for branching bisimulation, J. ACM, 42, 2, 458-487 (1995) · Zbl 0886.68064
[67] van Glabbeek, R. J.; Weijland, W. P., Branching time and abstraction in bisimulation semantics, J. ACM, 43, 3, 555-600 (1996) · Zbl 0882.68085
[68] Alur, R.; Henzinger, T. A.; Kupferman, O.; Vardi, M. Y., Alternating refinement relations, (CONCUR. CONCUR, LNCS, vol. 1466 (1998), Springer), 163-178 · Zbl 1070.68524
[69] van Benthem, J., Extensive games as process models, J. Log. Lang. Inf., 11, 3, 289-313 (2002) · Zbl 1003.03530
[70] Friedmann, O.; Lange, M., Solving parity games in practice, (ATVA. ATVA, LNCS, vol. 5799 (2009), Springer), 182-196 · Zbl 1258.68077
[71] Ummels, M.; Wojtczak, D., The complexity of Nash equilibria in stochastic multiplayer games, Log. Methods Comput. Sci., 7, 3, 1-45 (2011) · Zbl 1238.91025
[72] Ågotnes, T.; van der Hoek, W.; Wooldridge, M., Reasoning about coalitional games, Artif. Intell., 173, 1, 45-79 (2009) · Zbl 1180.68271
[73] Belardinelli, F.; Lomuscio, A.; Murano, A.; Rubin, S., Verification of multi-agent systems with imperfect information and public actions, (AAMAS (2017), ACM), 1268-1276
[74] Aminof, B.; Mogavero, F.; Murano, A., Synthesis of hierarchical systems, Sci. Comput. Program., 83, 56-79 (2014)
[75] Berthon, R.; Maubert, B.; Murano, A., Decidability results for ATL* with imperfect information and perfect recall, (AAMAS (2017), ACM), 1250-1258
[76] Herzig, A.; Lorini, E.; Maffre, F.; Schwarzentruber, F., Epistemic Boolean games based on a logic of visibility and control, (IJCAI (2016), IJCAI/AAAI Press), 1116-1122
[77] Belardinelli, F.; Lomuscio, A., Quantified epistemic logics for reasoning about knowledge in multi-agent systems, Artif. Intell., 173, 9-10, 982-1013 (2009) · Zbl 1191.68646
[78] Gutierrez, J.; Murano, A.; Perelli, G.; Rubin, S.; Wooldridge, M. J., Nash equilibria in concurrent games with lexicographic preferences, (IJCAI (2017)), 1067-1073, ijcai.org
[79] Almagor, S.; Kupferman, O.; Perelli, G., Synthesis of controllable Nash equilibria in quantitative objective game, (Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence. Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence, IJCAI 2018, July 13-19, 2018, Stockholm, Sweden (2018)), 35-41
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.