Abstract
Game-theoretic techniques and equilibria analysis facilitate the design and verification of competitive systems. While algorithmic complexity of equilibria computation has been extensively studied, practical implementation and application of game-theoretic methods is more recent. Tools such as PRISM-games support automated verification and synthesis of zero-sum and (\(\varepsilon \)-optimal subgame-perfect) social welfare Nash equilibria properties for concurrent stochastic games. However, these methods become inefficient as the number of agents grows and may also generate equilibria that yield significant variations in the outcomes for individual agents. We extend the functionality of PRISM-games to support correlated equilibria, in which players can coordinate through public signals, and introduce a novel optimality criterion of social fairness, which can be applied to both Nash and correlated equilibria. We show that correlated equilibria are easier to compute, are more equitable, and can also improve joint outcomes. We implement algorithms for both normal form games and the more complex case of multi-player concurrent stochastic games with temporal logic specifications. On a range of case studies, we demonstrate the benefits of our methods.
Chapter PDF
Similar content being viewed by others
References
de Alfaro, L.: Formal Verification of Probabilistic Systems. Ph.D. thesis, Stanford University (1997)
Aminof, B., Kwiatkowska, M., B. Maubert, B., Murano, A., Rubin, S.: Probabilistic strategy logic. In: Proc. IJCAI’19. pp. 32–38 (2019)
Aumann, R.: Subjectivity and correlation in randomized strategies. Journal of Mathematical Economics 1(1), 67–96 (1974)
Baier, C., Katoen, J.P.: Principles of Model Checking. MIT Press (2008)
Baier, C., Kwiatkowska, M.: Model checking for a probabilistic branching time logic with fairness. Distributed Computing 11(3), 125–155 (1998)
Banerjee, T., Majumdar, R., Mallik, K., Schmuck, A.K., Soudjani, S.: Fast symbolic algorithms for omega-regular games under strong transition fairness. Tech. Rep. MPI-SWS-2020-007r, Max Planck Institute (2021)
Brenguier, R.: PRALINE: A tool for computing Nash equilibria in concurrent games. In: Sharygina, N., Veith, H. (eds.) Proc. CAV’13. LNCS, vol. 8044, pp. 890–895. Springer (2013), lsv.fr/Software/praline/
Chatterjee, K., Fijalkow, N.: A reduction from parity games to simple stochastic games. EPTCS 54, 74–86 (2011)
Chatterjee, K., Henzinger, T.: Value iteration. In: 25 Years of Model Checking. LNCS, vol. 5000, pp. 107–138. Springer (2008)
Chen, T., Forejt, V., Kwiatkowska, M., Parker, D., Simaitis, A.: Automatic verification of competitive stochastic systems. Formal Methods in System Design 43(1), 61–92 (2013)
Chen, X., Deng, X., Teng, S.H.: Settling the complexity of computing two-player Nash equilibria. J. ACM 56(3) (2009)
Daskalakis, C., Goldberg, P., Papadimitriou, C.: The complexity of computing a Nash equilibrium. Communications of the ACM 52(2), 89–97 (2009)
De Moura, L., Bjørner, N.: Z3: An efficient SMT solver. In: Proc. TACAS’08. LNCS, vol. 4963, pp. 337–340. Springer (2008), github.com/Z3Prover/z3
Dutertre, B.: Yices 2.2. In: Biere, A., Bloem, R. (eds.) Proc CAV’14. LNCS, vol. 8559, pp. 737–744. Springer (2014), yices.csl.sri.com
Gilboa, I., Zemel, E.: Nash and correlated equilibria: Some complexity considerations. Games and Economic Behavior 1(1), 80–93 (1989)
Griva, I., Nash, S., Sofer, A.: Linear and Nonlinear Optimization: Second Edition. CUP (01 2009)
Gurobi Optimization, LLC: Gurobi Optimizer Reference Manual (2021), www.gurobi.com
Gutierrez, J., Harrenstein, P., Wooldridge, M.J.: Reasoning about equilibria in game-like concurrent systems. In: Proc. 14th International Conference on Principles of Knowledge Representation and Reasoning (KR’14) (2014)
Hauser, O., Hilbe, C., Chatterjee, K., Nowak, M.: Social dilemmas among unequals. Nature 572, 524–527 (2019)
Kemeny, J., Snell, J., Knapp, A.: Denumerable Markov Chains. Springer (1976)
Kwiatkowska, M., Norman, G., Parker, D., Santos, G.: Multi-player equilibria verification for concurrent stochastic games. In: Gribaudo, M., Jansen, D., Remke, A. (eds.) Proc. QEST’20. LNCS, Springer (2020)
Kwiatkowska, M., Norman, G., Parker, D., Santos, G.: PRISM-games 3.0: Stochastic game verification with concurrency, equilibria and time. In: Proc. CAV’20. pp. 475–487. LNCS, Springer (2020)
Kwiatkowska, M., Norman, G., Parker, D., Santos, G.: Correlated equilibria and fairness in concurrent stochastic games (2022), arXiv:2201.09702
Kwiatkowska, M., Norman, G., Parker, D., Santos, G.: Automatic verification of concurrent stochastic systems. Formal Methods in System Design pp. 1–63 (2021)
Littman, M., Ravi, N., Talwar, A., Zinkevich, M.: An efficient optimal-equilibrium algorithm for two-player game trees. In: Proc. UAI’06. pp. 298–305. AUAI Press (2006)
McIver, A., Morgan, C.: Results on the quantitative mu-calculus qMu. ACM Trans. Computational Logic 8(1) (2007)
von Neumann, J., Morgenstern, O., Kuhn, H., Rubinstein, A.: Theory of Games and Economic Behavior. Princeton University Press (1944)
Nisan, N., Roughgarden, T., Tardos, E., Vazirani, V.: Algorithmic Game Theory. CUP (2007)
Nudelman, E., Wortman, J., Shoham, Y., Leyton-Brown, K.: Run the GAMUT: A comprehensive approach to evaluating game-theoretic algorithms. In: Proc. AAMAS’04. pp. 880–887. ACM (2004), gamut.stanford.edu
Osborne, M., Rubinstein, A.: An Introduction to Game Theory. OUP (2004)
Porter, R., Nudelman, E., Shoham, Y.: Simple search methods for finding a Nash equilibrium. In: Proc. AAAI’04. pp. 664–669. AAAI Press (2004)
Prisner, E.: Game Theory Through Examples. Mathematical Association of America, 1 edn. (2014)
Rabin, M.: Incorporating fairness into game theory and economics. The American Economic Review 83(5), 1281–1302 (1993)
Rabin, M.: Fairness in repeated games. working paper 97–252, University of California at Berkeley (1997)
Schwalbe, U., Walker, P.: Zermelo and the early history of game theory. Games and Economic Behavior 34(1), 123–137 (2001)
Shapley, L.: Stochastic games. PNAS 39, 1095–1100 (1953)
Stevens, S., Palocsay, S.: Teaching use of binary variables in integer linear programs: Formulating logical conditions. INFORMS Transactions on Education 18(1), 28–36 (2017)
Wächter, A.: Short tutorial: Getting started with ipopt in 90 minutes. In: Combinatorial Scientific Computing. No. 09061 in Dagstuhl Seminar Proceedings, Leibniz-Zentrum für Informatik (2009), github.com/coin-or/Ipopt
Wächter, A., Biegler, L.: On the implementation of an interior-point filter line-search algorithm for large-scale nonlinear programming. Mathematical Programming 106(1), 25–57 (2006)
Supporting material, www.prismmodelchecker.org/files/tacas22equ/
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), 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 license and indicate if changes were made.
The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license 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.
Copyright information
© 2022 The Author(s)
About this paper
Cite this paper
Kwiatkowska, M., Norman, G., Parker, D., Santos, G. (2022). Correlated Equilibria and Fairness in Concurrent Stochastic Games. In: Fisman, D., Rosu, G. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2022. Lecture Notes in Computer Science, vol 13244. Springer, Cham. https://doi.org/10.1007/978-3-030-99527-0_4
Download citation
DOI: https://doi.org/10.1007/978-3-030-99527-0_4
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-99526-3
Online ISBN: 978-3-030-99527-0
eBook Packages: Computer ScienceComputer Science (R0)