Skip to main content

Multi-player Equilibria Verification for Concurrent Stochastic Games

  • Conference paper
  • First Online:
Quantitative Evaluation of Systems (QEST 2020)

Abstract

Concurrent stochastic games (CSGs) are an ideal formalism for modelling probabilistic systems that feature multiple players or components with distinct objectives making concurrent, rational decisions. Examples include communication or security protocols and multi-robot navigation. Verification methods for CSGs exist but are limited to scenarios where agents or players are grouped into two coalitions, with those in the same coalition sharing an identical objective. In this paper, we propose multi-coalitional verification techniques for CSGs. We use subgame-perfect social welfare (or social cost) optimal Nash equilibria, which are strategies where there is no incentive for any coalition to unilaterally change its strategy in any game state, and where the total combined objectives are maximised (or minimised). We present an extension of the temporal logic rPATL (probabilistic alternating-time temporal logic with rewards) to specify equilibria-based properties for any number of distinct coalitions, and a corresponding model checking algorithm for a variant of stopping games. We implement our techniques in the PRISM-games tool and apply them to several case studies, including a secret sharing protocol and a public good game.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Similar content being viewed by others

Notes

  1. 1.

    For each \(i \in N\) this can be any action in \(B_i\).

References

  1. de Alfaro, L.: Formal verification of probabilistic systems. Ph.D. thesis, Stanford University (1997)

    Google Scholar 

  2. de Alfaro, L., Henzinger, T., Kupferman, O.: Concurrent reachability games. Theoret. Comput. Sci. 386(3), 188–217 (2007)

    Article  MathSciNet  Google Scholar 

  3. de Alfaro, L., Majumdar, R.: Quantitative solution of omega-regular games. J. Comput. Syst. Sci. 68(2), 374–397 (2004)

    Article  MathSciNet  Google Scholar 

  4. Alur, R., Henzinger, T.A., Kupferman, O.: Alternating-time temporal logic. J. ACM 49(5), 672–713 (2002)

    Article  MathSciNet  Google Scholar 

  5. Aumann, R.: Subjectivity and correlation in randomized strategies. J. Math. Econ. 1(1), 67–96 (1974)

    Article  MathSciNet  Google Scholar 

  6. Bouyer, P., Markey, N., Stan, D.: Mixed Nash equilibria in concurrent games. In: Proceedings of FSTTCS 2014, LIPICS, vol. 29, pp. 351–363. Leibniz-Zentrum für Informatik (2014)

    Google Scholar 

  7. Brenguier, R.: PRALINE: a tool for computing Nash equilibria in concurrent games. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 890–895. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-39799-8_63

    Chapter  Google Scholar 

  8. Brihaye, T., Bruyère, V., Goeminne, A., Raskin, J.F., van den Bogaard, M.: The complexity of subgame perfect equilibria in quantitative reachability games. In: Proceedings of CONCUR 2019, LIPICS, vol. 140, pp. 13:1–13:16. Leibniz-Zentrum für Informatik (2019)

    Google Scholar 

  9. Čermák, P., Lomuscio, A., Mogavero, F., Murano, A.: MCMAS-SLK: a model checker for the verification of strategy logic specifications. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 525–532. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-08867-9_34

    Chapter  Google Scholar 

  10. Chatterjee, K., de Alfaro, L., Henzinger, T.: Strategy improvement for concurrent reachability and turn-based stochastic safety games. J. Comput. Syst. Sci. 79(5), 640–657 (2013)

    Article  MathSciNet  Google Scholar 

  11. Chatterjee, K., Henzinger, T.A.: Value iteration. In: Grumberg, O., Veith, H. (eds.) 25 Years of Model Checking. LNCS, vol. 5000, pp. 107–138. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-69850-0_7

    Chapter  Google Scholar 

  12. Chen, T., Forejt, V., Kwiatkowska, M., Parker, D., Simaitis, A.: Automatic verification of competitive stochastic systems. Formal Methods Syst. Design 43(1), 61–92 (2013)

    Article  Google Scholar 

  13. Chen, T., Forejt, V., Kwiatkowska, M., Simaitis, A., Wiltsche, C.: On stochastic games with multiple objectives. In: Chatterjee, K., Sgall, J. (eds.) MFCS 2013. LNCS, vol. 8087, pp. 266–277. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-40313-2_25

    Chapter  Google Scholar 

  14. Cramton, P., Shoham, Y., Steinberg, R.: An overview of combinatorial auctions. SIGecom Exchanges 7, 3–14 (2007)

    Article  Google Scholar 

  15. Daskalakis, C., Goldberg, P., Papadimitriou, C.: The complexity of computing a Nash equilibrium. Commun. ACM 52(2), 89–97 (2009)

    Article  Google Scholar 

  16. de Moura, L., Bjørner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-78800-3_24

    Chapter  Google Scholar 

  17. Govindan, S., Wilson, R.: A global newton method to compute Nash equilibria. J. Econ. Theory 110(1), 65–86 (2003)

    Article  MathSciNet  Google Scholar 

  18. Gutierrez, J., Najib, M., Perelli, G., Wooldridge, M.: EVE: a tool for temporal equilibrium analysis. In: Lahiri, S.K., Wang, C. (eds.) ATVA 2018. LNCS, vol. 11138, pp. 551–557. Springer, Cham (2018). https://doi.org/10.1007/978-3-030-01090-4_35

    Chapter  Google Scholar 

  19. Halpern, J., Teague, V.: Rational secret sharing and multiparty computation: extended abstract. In: Proceedings of STOC 2004, pp. 623–632. ACM (2004)

    Google Scholar 

  20. Hauser, O., Hilbe, C., Chatterjee, K., Nowak, M.: Social dilemmas among unequals. Nature 572, 524–527 (2019)

    Article  Google Scholar 

  21. Kemeny, J., Snell, J., Knapp, A.: Denumerable Markov Chains. Springer, New York (1976). https://doi.org/10.1007/978-1-4684-9455-6

    Book  MATH  Google Scholar 

  22. Kwiatkowska, M., Norman, G., Parker, D., Santos, G.: Automated verification of concurrent stochastic games. In: McIver, A., Horvath, A. (eds.) QEST 2018. LNCS, vol. 11024, pp. 223–239. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-99154-2_14

    Chapter  Google Scholar 

  23. Kwiatkowska, M., Norman, G., Parker, D., Santos, G.: Equilibria-based probabilistic model checking for concurrent stochastic games. In: ter Beek, M.H., McIver, A., Oliveira, J.N. (eds.) FM 2019. LNCS, vol. 11800, pp. 298–315. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-30942-8_19

    Chapter  Google Scholar 

  24. Kwiatkowska, M., Norman, G., Parker, D., Santos, G.: Multi-player equilibria verification for concurrent stochastic games (2020). arXiv:2007.03365

  25. Kwiatkowska, M., Norman, G., Parker, D., Santos, G.: PRISM-games 3.0: stochastic game verification with concurrency, equilibria and time. In: Proceedings of CAV 2020, LNCS. Springer (2020, to appear). http://www.prismmodelchecker.org/games

  26. McKelvey, R., McLennan, A., Turocy, T.: Gambit: software tools for game theory, version 16.0.1 (2016). http://www.gambit-project.org

  27. Narahari, Y., Narayanam, R., Garg, D., Prakash, H.: Foundations of mechanism design. In: Game Theoretic Problems in Network Economics and Mechanism Design Solutions, Advanced Information and Knowledge Processing, pp. 1–131. Springer, London (2009). https://doi.org/10.1007/978-1-84800-938-7_2

  28. von Neumann, J., Morgenstern, O., Kuhn, H., Rubinstein, A.: Theory of Games and Economic Behavior. Princeton University Press, Princeton (1944)

    Google Scholar 

  29. Nisan, N., Roughgarden, T., Tardos, E., Vazirani, V.: Algorithmic Game Theory. CUP, Cambridge (2007)

    Book  Google Scholar 

  30. Nocedal, J., Wächter, A., Waltz, R.: Adaptive barrier update strategies for nonlinear interior methods. SIAM J. Optim. 19(4), 1674–1693 (2009)

    Article  MathSciNet  Google Scholar 

  31. Nudelman, E., Wortman, J., Shoham, Y., Leyton-Brown, K.: Run the GAMUT: a comprehensive approach to evaluating game-theoretic algorithms. In: Proceedings of AAMAS 2004, pp. 880–887. ACM (2004). http://www.gamut.stanford.edu

  32. Osborne, M., Rubinstein, A.: An Introduction to Game Theory. OUP, Oxford (2004)

    Google Scholar 

  33. Porter, R., Nudelman, E., Shoham, Y.: Simple search methods for finding a Nash equilibrium. In: Proceedings of AAAI 2004, pp. 664–669. AAAI Press (2004)

    Google Scholar 

  34. Roughgarden, T., Tardos, E.: How bad is selfish routing? J. ACM 49, 236–259 (2002)

    Article  MathSciNet  Google Scholar 

  35. Schwalbe, U., Walker, P.: Zermelo and the early history of game theory. Games Econ. Behav. 34(1), 123–137 (2001)

    Article  MathSciNet  Google Scholar 

  36. Shimoji, M., Watson, J.: Conditional dominance, rationalizability, and game forms. J. Econ. Theory 83, 161–195 (1998)

    Article  MathSciNet  Google Scholar 

  37. Toumi, A., Gutierrez, J., Wooldridge, M.: A tool for the automated verification of Nash equilibria in concurrent games. In: Leucker, M., Rueda, C., Valencia, F.D. (eds.) ICTAC 2015. LNCS, vol. 9399, pp. 583–594. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-25150-9_34

    Chapter  MATH  Google Scholar 

  38. Van Der Laan, G., Talman, A., Van Der Heyden, L.: Simplicial variable dimension algorithms for solving the nonlinear complementarity problem on a product of unit simplices using a general labelling. Math. Oper. Res. 12(3), 377–397 (1987)

    Article  MathSciNet  Google Scholar 

  39. 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). http://www.github.com/coin-or/Ipopt

  40. Wächter, A., Biegler, L.: On the implementation of an interior-point filter line-search algorithm for large-scale nonlinear programming. Math. Program. 106(1), 25–57 (2006)

    Article  MathSciNet  Google Scholar 

  41. Supporting material. http://www.prismmodelchecker.org/files/qest20

Download references

Acknowledgements

This project has received funding from the European Research Council (ERC) under the European Union’s Horizon 2020 research and innovation programme (grant agreement No. 834115) and the EPSRC Programme Grant on Mobile Autonomy (EP/M019918/1).

Author information

Authors and Affiliations

Authors

Corresponding author

Correspondence to Gethin Norman .

Editor information

Editors and Affiliations

Rights and permissions

Reprints and permissions

Copyright information

© 2020 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Kwiatkowska, M., Norman, G., Parker, D., Santos, G. (2020). Multi-player Equilibria Verification for Concurrent Stochastic Games. In: Gribaudo, M., Jansen, D.N., Remke, A. (eds) Quantitative Evaluation of Systems. QEST 2020. Lecture Notes in Computer Science(), vol 12289. Springer, Cham. https://doi.org/10.1007/978-3-030-59854-9_7

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-59854-9_7

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-59853-2

  • Online ISBN: 978-3-030-59854-9

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics