Advertisement

Equilibria-Based Probabilistic Model Checking for Concurrent Stochastic Games

  • Marta Kwiatkowska
  • Gethin NormanEmail author
  • David Parker
  • Gabriel Santos
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11800)

Abstract

Probabilistic model checking for stochastic games enables formal verification of systems that comprise competing or collaborating entities operating in a stochastic environment. Despite good progress in the area, existing approaches focus on zero-sum goals and cannot reason about scenarios where entities are endowed with different objectives. In this paper, we propose probabilistic model checking techniques for concurrent stochastic games based on Nash equilibria. We extend the temporal logic rPATL (probabilistic alternating-time temporal logic with rewards) to allow reasoning about players with distinct quantitative goals, which capture either the probability of an event occurring or a reward measure. We present algorithms to synthesise strategies that are subgame perfect social welfare optimal Nash equilibria, i.e., where there is no incentive for any players to unilaterally change their strategy in any state of the game, whilst the combined probabilities or rewards are maximised. We implement our techniques in the PRISM-games tool and apply them to several case studies, including network protocols and robot navigation, showing the benefits compared to existing approaches.

Notes

Acknowledgements

This work is partially supported by the EPSRC Programme Grant on Mobile Autonomy and the PRINCESS project, under the DARPA BRASS programme. We would like to thank the reviewers of an earlier version of this paper for finding a flaw in the correctness proof.

References

  1. 1.
    de Alfaro, L.: Computing minimum and maximum reachability times in probabilistic systems. In: Baeten, J.C.M., Mauw, S. (eds.) CONCUR 1999. LNCS, vol. 1664, pp. 66–81. Springer, Heidelberg (1999).  https://doi.org/10.1007/3-540-48320-9_7CrossRefGoogle Scholar
  2. 2.
    de Alfaro, L., Henzinger, T., Kupferman, O.: Concurrent reachability games. Theor. Comput. Sci. 386(3), 188–217 (2007)MathSciNetCrossRefGoogle Scholar
  3. 3.
    de Alfaro, L., Majumdar, R.: Quantitative solution of omega-regular games. J. Comput. Syst. Sci. 68(2), 374–397 (2004)MathSciNetCrossRefGoogle Scholar
  4. 4.
    Alur, R., Henzinger, T.A., Kupferman, O.: Alternating-time temporal logic. J. ACM 49(5), 672–713 (2002)MathSciNetCrossRefGoogle Scholar
  5. 5.
    Arslan, G., Yüksel, S.: Distributionally consistent price taking equilibria in stochastic dynamic games. In: Proceedings of CDC 2017, pp. 4594–4599. IEEE (2017)Google Scholar
  6. 6.
    Basset, N., Kwiatkowska, M., Wiltsche, C.: Compositional strategy synthesis for stochastic games with multiple objectives. Inf. Comput. 261(3), 536–587 (2018)MathSciNetCrossRefGoogle Scholar
  7. 7.
    Bianco, A., de Alfaro, L.: Model checking of probabilistic and nondeterministic systems. In: Thiagarajan, P.S. (ed.) FSTTCS 1995. LNCS, vol. 1026, pp. 499–513. Springer, Heidelberg (1995).  https://doi.org/10.1007/3-540-60692-0_70CrossRefzbMATHGoogle Scholar
  8. 8.
    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
  9. 9.
    Bouyer, P., Markey, N., Stan, D.: Stochastic equilibria under imprecise deviations in terminal-reward concurrent games. In: Proceedings of GandALF 2016, EPTCS, vol. 226, pp. 61–75. Open Publishing Association (2016)Google Scholar
  10. 10.
    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_63CrossRefGoogle Scholar
  11. 11.
    Č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_34CrossRefGoogle Scholar
  12. 12.
    Chatterjee, K.: Nash equilibrium for upward-closed objectives. In: Ésik, Z. (ed.) CSL 2006. LNCS, vol. 4207, pp. 271–286. Springer, Heidelberg (2006).  https://doi.org/10.1007/11874683_18CrossRefGoogle Scholar
  13. 13.
    Chatterjee, K.: Stochastic \(\omega \)-regular games. Ph.D. thesis, University of California at Berkeley (2007)Google Scholar
  14. 14.
    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)MathSciNetCrossRefGoogle Scholar
  15. 15.
    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_7CrossRefGoogle Scholar
  16. 16.
    Chatterjee, K., Majumdar, R., Jurdziński, M.: On Nash equilibria in stochastic games. In: Marcinkowski, J., Tarlecki, A. (eds.) CSL 2004. LNCS, vol. 3210, pp. 26–40. Springer, Heidelberg (2004).  https://doi.org/10.1007/978-3-540-30124-0_6CrossRefGoogle Scholar
  17. 17.
    Chen, T., Forejt, V., Kwiatkowska, M., Parker, D., Simaitis, A.: Automatic verification of competitive stochastic systems. Formal Methods Syst. Des. 43(1), 61–92 (2013)CrossRefGoogle Scholar
  18. 18.
    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_25CrossRefGoogle Scholar
  19. 19.
    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_24CrossRefGoogle Scholar
  20. 20.
    Dehnert, C., Junges, S., Katoen, J.-P., Volk, M.: A Storm is coming: a modern probabilistic model checker. In: Majumdar, R., Kunčak, V. (eds.) CAV 2017. LNCS, vol. 10427, pp. 592–600. Springer, Cham (2017).  https://doi.org/10.1007/978-3-319-63390-9_31CrossRefGoogle Scholar
  21. 21.
    Fernando, D., Dong, N., Jegourel, C., Dong, J.S.: Verification of strong Nash-equilibrium for probabilistic BAR systems. In: Sun, J., Sun, M. (eds.) ICFEM 2018. LNCS, vol. 11232, pp. 106–123. Springer, Cham (2018).  https://doi.org/10.1007/978-3-030-02450-5_7CrossRefGoogle Scholar
  22. 22.
    Haddad, S., Monmege, B.: Interval iteration algorithm for MDPs and IMDPs. Theor. Comput. Sci. 735, 111–131 (2018)MathSciNetCrossRefGoogle Scholar
  23. 23.
    Hansson, H., Jonsson, B.: A logic for reasoning about time and reliability. Formal Aspects Comput. 6(5), 512–535 (1994)CrossRefGoogle Scholar
  24. 24.
    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_35CrossRefGoogle Scholar
  25. 25.
    Kelmendi, E., Krämer, J., Křetínský, J., Weininger, M.: Value iteration for simple stochastic games: stopping criterion and learning algorithm. In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018. LNCS, vol. 10981, pp. 623–642. Springer, Cham (2018).  https://doi.org/10.1007/978-3-319-96145-3_36 CrossRefGoogle Scholar
  26. 26.
    Kemeny, J., Snell, J., Knapp, A.: Denumerable Markov Chains. Springer, New York (1976).  https://doi.org/10.1007/978-1-4684-9455-6CrossRefzbMATHGoogle Scholar
  27. 27.
    Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 585–591. Springer, Heidelberg (2011).  https://doi.org/10.1007/978-3-642-22110-1_47CrossRefGoogle Scholar
  28. 28.
    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_14CrossRefGoogle Scholar
  29. 29.
    Kwiatkowska, M., Norman, G., Parker, D., Santos, G.: Equilibria-based probabilistic model checking for concurrent stochastic games (2018). http://arxiv.org/abs/1811.07145
  30. 30.
    Kwiatkowska, M., Parker, D.: Automated verification and strategy synthesis for probabilistic systems. In: Van Hung, D., Ogawa, M. (eds.) ATVA 2013. LNCS, vol. 8172, pp. 5–22. Springer, Cham (2013).  https://doi.org/10.1007/978-3-319-02444-8_2CrossRefzbMATHGoogle Scholar
  31. 31.
    Kwiatkowska, M., Parker, D., Wiltsche, C.: PRISM-games: verification and strategy synthesis for stochastic multi-player games with multiple objectives. Softw. Tools Technol. Transf. 20(2), 195–210 (2018)CrossRefGoogle Scholar
  32. 32.
    Lemke, C., Howson Jr., J.: Equilibrium points of bimatrix games. J. Soc. Ind. Appl. Math. 12(2), 413–423 (1964)MathSciNetCrossRefGoogle Scholar
  33. 33.
    Lozovanu, D., Pickl, S.: Determining Nash equilibria for stochastic positional games with discounted payoffs. In: Rothe, J. (ed.) ADT 2017. LNCS (LNAI), vol. 10576, pp. 339–343. Springer, Cham (2017).  https://doi.org/10.1007/978-3-319-67504-6_24CrossRefGoogle Scholar
  34. 34.
    McKelvey, R., McLennan, A., Turocy, T.: Gambit: software tools for game theory, version 16.0.1 (2016). gambit-project.org
  35. 35.
    von Neumann, J., Morgenstern, O., Kuhn, H., Rubinstein, A.: Theory of Games and Economic Behavior. Princeton University Press, Princeton (1944)Google Scholar
  36. 36.
    Nisan, N., Roughgarden, T., Tardos, E., Vazirani, V.: Algorithmic Game Theory. Cambridge University Press, Cambridge (2007)CrossRefGoogle Scholar
  37. 37.
    Osborne, M., Rubinstein, A.: An Introduction to Game Theory. Oxford University Press, Oxford (2004)Google Scholar
  38. 38.
    Pacheco, J., Santos, F., Souza, M., Skyrms, B.: Evolutionary dynamics of collective action. In: Chalub, F., Rodrigues, J. (eds.) The Mathematics of Darwin’s Legacy, pp. 119–138. Springer, Basel (2011).  https://doi.org/10.1007/978-3-0348-0122-5_7CrossRefGoogle Scholar
  39. 39.
    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
  40. 40.
    Prasad, H., Prashanth, L., Bhatnagar, S.: Two-timescale algorithms for learning Nash equilibria in general-sum stochastic games. In: Proceedings of AAMAS 2015, pp. 1371–1379. IFAAMAS (2015)Google Scholar
  41. 41.
    Sandholm, T., Gilpin, A., Conitzer, V.: Mixed-integer programming methods for finding Nash equilibria. In: Proceedings of AAAI 2005, pp. 495–501. AAAI Press (2005)Google Scholar
  42. 42.
    Schwalbe, U., Walker, P.: Zermelo and the early history of game theory. Games Econ. Behav. 34(1), 123–137 (2001)MathSciNetCrossRefGoogle Scholar
  43. 43.
    Shapley, L.: A note on the Lemke-Howson algorithm. In: Balinski, M.L. (ed.) Pivoting and Extension. Mathematical Programming Studies, vol. 1, pp. 175–189. Springer, Heidelberg (1974). In Honor of A.W. TuckerCrossRefGoogle Scholar
  44. 44.
    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_34CrossRefzbMATHGoogle Scholar
  45. 45.
    Ummels, M.: Stochastic multiplayer games: theory and algorithms. Ph.D. thesis, RWTH Aachen University (2010)Google Scholar
  46. 46.

Copyright information

© Springer Nature Switzerland AG 2019

Authors and Affiliations

  1. 1.Department of Computing ScienceUniversity of OxfordOxfordUK
  2. 2.School of Computing ScienceUniversity of GlasgowGlasgowUK
  3. 3.School of Computer ScienceUniversity of BirminghamBirminghamUK

Personalised recommendations