{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T09:58:54Z","timestamp":1776333534050,"version":"3.51.2"},"reference-count":81,"publisher":"Springer Science and Business Media LLC","issue":"1-2","license":[{"start":{"date-parts":[[2021,1,22]],"date-time":"2021-01-22T00:00:00Z","timestamp":1611273600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2021,1,22]],"date-time":"2021-01-22T00:00:00Z","timestamp":1611273600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/100010663","name":"H2020 European Research Council","doi-asserted-by":"publisher","award":["834115"],"award-info":[{"award-number":["834115"]}],"id":[{"id":"10.13039\/100010663","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100000266","name":"Engineering and Physical Sciences Research Council","doi-asserted-by":"publisher","award":["EP\/M019918\/1"],"award-info":[{"award-number":["EP\/M019918\/1"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2021,10]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Automated verification techniques for stochastic games allow formal reasoning about systems that feature competitive or collaborative behaviour among rational agents in uncertain or probabilistic settings. Existing tools and techniques focus on turn-based games, where each state of the game is controlled by a single player, and on zero-sum properties, where two players or coalitions have directly opposing objectives. In this paper, we present automated verification techniques for concurrent stochastic games (CSGs), which provide a more natural model of concurrent decision making and interaction. We also consider (social welfare) Nash equilibria, to formally identify scenarios where two players or coalitions with distinct goals can collaborate to optimise their joint performance. We propose an extension of the temporal logic rPATL for specifying quantitative properties in this setting and present corresponding algorithms for verification and strategy synthesis for a variant of stopping games. For finite-horizon properties the computation is exact, while for infinite-horizon it is approximate using value iteration. For zero-sum properties it requires solving matrix games via linear programming, and for equilibria-based properties we find social welfare or social cost Nash equilibria of bimatrix games via the method of labelled polytopes through an SMT encoding. We implement this approach in PRISM-games, which required extending the tool\u2019s modelling language for CSGs, and apply it to case studies from domains including robotics, computer security and computer networks, explicitly demonstrating the benefits of both CSGs and equilibria-based properties.\n<\/jats:p>","DOI":"10.1007\/s10703-020-00356-y","type":"journal-article","created":{"date-parts":[[2021,1,22]],"date-time":"2021-01-22T12:10:04Z","timestamp":1611317404000},"page":"188-250","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":21,"title":["Automatic verification of concurrent stochastic systems"],"prefix":"10.1007","volume":"58","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9022-7599","authenticated-orcid":false,"given":"Marta","family":"Kwiatkowska","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9326-4344","authenticated-orcid":false,"given":"Gethin","family":"Norman","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4137-8862","authenticated-orcid":false,"given":"David","family":"Parker","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6570-9737","authenticated-orcid":false,"given":"Gabriel","family":"Santos","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2021,1,22]]},"reference":[{"issue":"5","key":"356_CR1","doi-asserted-by":"publisher","first-page":"672","DOI":"10.1145\/585265.585270","volume":"49","author":"R Alur","year":"2002","unstructured":"Alur R, Henzinger T, Kupferman O (2002) Alternating-time temporal logic. J ACM 49(5):672\u2013713","journal-title":"J ACM"},{"key":"356_CR2","doi-asserted-by":"crossref","unstructured":"Arslan G, Y\u00fcksel S (2017) Distributionally consistent price taking equilibria in stochastic dynamic games. In: Proceedings of CDC\u201917. IEEE, pp 4594\u20134599","DOI":"10.1109\/CDC.2017.8264338"},{"key":"356_CR3","doi-asserted-by":"crossref","unstructured":"Ashok P, Chatterjee K, Kret\u00ednsk\u00fd J, Weininger M, Winkler T (2020) Approximating values of generalized-reachability stochastic games. In: Proceedings of LICS\u201920. ACM, pp 102\u2013115","DOI":"10.1145\/3373718.3394761"},{"issue":"1","key":"356_CR4","doi-asserted-by":"publisher","first-page":"9","DOI":"10.1007\/s00199-009-0449-x","volume":"42","author":"D Avis","year":"2010","unstructured":"Avis D, Rosenberg G, Savani R, von Stengel B (2010) Enumeration of Nash equilibria for two-player games. Econ Theory 42(1):9\u201337","journal-title":"Econ Theory"},{"issue":"3","key":"356_CR5","doi-asserted-by":"publisher","first-page":"536","DOI":"10.1016\/j.ic.2017.09.010","volume":"261","author":"N Basset","year":"2018","unstructured":"Basset N, Kwiatkowska M, Wiltsche C (2018) Compositional strategy synthesis for stochastic games with multiple objectives. Inf Comput 261(3):536\u2013587","journal-title":"Inf Comput"},{"key":"356_CR6","doi-asserted-by":"crossref","unstructured":"Bianco A, de\u00a0Alfaro L (1995) Model checking of probabilistic and nondeterministic systems. In: Thiagarajan P (ed) Proceedings of FSTTCS\u201995, LNCS, vol 1026. Springer, pp 499\u2013513","DOI":"10.1007\/3-540-60692-0_70"},{"key":"356_CR7","unstructured":"Bouyer P, Markey N, Stan D (2014) Mixed Nash equilibria in concurrent games. In: Raman V, Suresh S (eds) Proceedings of FSTTCS\u201914, LIPICS, vol\u00a029. Leibniz-Zentrum f\u00fcr Informatik, pp 351\u2013363"},{"key":"356_CR8","doi-asserted-by":"crossref","unstructured":"Bouyer P, Markey N, Stan D (2016) Stochastic equilibria under imprecise deviations in terminal-reward concurrent games. In: Cantone D, Delzanno G (eds) Proceedings of GandALF\u201916, EPTCS, vol 226. Open Publishing Association, pp 61\u201375","DOI":"10.4204\/EPTCS.226.5"},{"key":"356_CR9","doi-asserted-by":"crossref","unstructured":"Br\u00e1zdil T, Chatterjee K, Chmel\u00edk M, Forejt V, K\u0159et\u00ednsk\u00fd J, Kwiatkowska M, Parker D, Ujma M (2014) Verification of Markov decision processes using learning algorithms. In: Cassez F, Raskin JF (eds) Proceedings of ATVA\u201914, LNCS, vol 8837. Springer, pp 98\u2013114","DOI":"10.1007\/978-3-319-11936-6_8"},{"key":"356_CR10","doi-asserted-by":"crossref","unstructured":"Brenguier R (2013) PRALINE: a tool for computing Nash equilibria in concurrent games. In: Sharygina N, Veith H (eds) Proceedings of CAV\u201913, LNCS, vol 8044. Springer, pp 890\u2013895. http:\/\/lsv.fr\/Software\/praline\/","DOI":"10.1007\/978-3-642-39799-8_63"},{"key":"356_CR11","unstructured":"Brihaye T, Bruy\u00e8re V, Goeminne A, Raskin JF, van\u00a0den Bogaard M (2019) The complexity of subgame perfect equilibria in quantitative reachability games. In: Fokkink W, van Glabbeek R (eds) Proceedings of CONCUR\u201919, LIPIcs, vol 140. Leibniz-Zentrum f\u00fcr Informatik, pp 13:1\u201313:16"},{"key":"356_CR12","doi-asserted-by":"crossref","unstructured":"\u010cerm\u00e1k P, Lomuscio A, Mogavero F, Murano A (2014) MCMAS-SLK: a model checker for the verification of strategy logic specifications. In: Biere A, Bloem R (eds) Proceedings of CAV\u201914, LNCS, vol 8559. Springer, pp 525\u2013532","DOI":"10.1007\/978-3-319-08867-9_34"},{"key":"356_CR13","unstructured":"Chatterjee K (2007) Stochastic $$\\omega $$-regular games. Ph.D. thesis, University of California at Berkeley"},{"issue":"5","key":"356_CR14","doi-asserted-by":"publisher","first-page":"640","DOI":"10.1016\/j.jcss.2012.12.001","volume":"79","author":"K Chatterjee","year":"2013","unstructured":"Chatterjee K, de Alfaro L, Henzinger T (2013) Strategy improvement for concurrent reachability and turn-based stochastic safety games. J Comput Syst Sci 79(5):640\u2013657","journal-title":"J Comput Syst Sci"},{"key":"356_CR15","doi-asserted-by":"crossref","unstructured":"Chatterjee K, Henzinger T (2008) Value iteration. In: Grumberg O, Veith H (eds) 25 years of model checking, LNCS, vol 5000. Springer, pp 107\u2013138","DOI":"10.1007\/978-3-540-69850-0_7"},{"issue":"2","key":"356_CR16","doi-asserted-by":"publisher","first-page":"394","DOI":"10.1016\/j.jcss.2011.05.002","volume":"78","author":"K Chatterjee","year":"2012","unstructured":"Chatterjee K, Henzinger T (2012) A survey of stochastic $$\\omega $$-regular games. J Comput Syst Sci 78(2):394\u2013413","journal-title":"J Comput Syst Sci"},{"key":"356_CR17","doi-asserted-by":"crossref","unstructured":"Chatterjee K, Henzinger T, Jobstmann B, Radhakrishna A (2010) Gist: a solver for probabilistic games. In: Touili T, Cook B, Jackson P (eds) Proceedings of CAV\u201910, LNCS, vol 6174. Springer, pp 665\u2013669. http:\/\/pub.ist.ac.at\/gist\/","DOI":"10.1007\/978-3-642-14295-6_57"},{"key":"356_CR18","doi-asserted-by":"crossref","unstructured":"Chatterjee K, Majumdar R, Jurdzi\u0144ski M (2004) On Nash equilibria in stochastic games. In: Marcinkowski J, Tarlecki A (eds) Proceedings of CSL\u201904, LNCS, vol 3210. Springer, pp 26\u201340","DOI":"10.1007\/978-3-540-30124-0_6"},{"issue":"1","key":"356_CR19","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1007\/s10703-013-0183-7","volume":"43","author":"T Chen","year":"2013","unstructured":"Chen T, Forejt V, Kwiatkowska M, Parker D, Simaitis A (2013) Automatic verification of competitive stochastic systems. Formal Methods Syst Des 43(1):61\u201392","journal-title":"Formal Methods Syst Des"},{"key":"356_CR20","doi-asserted-by":"crossref","unstructured":"Chen T, Forejt V, Kwiatkowska M, Simaitis A, Wiltsche C (2013) On stochastic games with multiple objectives. In: Chatterjee K, Sgall J (eds) Proceedings of MFCS\u201913, LNCS, vol 8087. Springer, pp 266\u2013277","DOI":"10.1007\/978-3-642-40313-2_25"},{"key":"356_CR21","doi-asserted-by":"crossref","unstructured":"Cheng C, Knoll A, Luttenberger M, Buckl C (2011) GAVS+: an open platform for the research of algorithmic game solving. In: Abdulla P, Leino K (eds) Proceedings of TACAS\u201911, LNCS, vol 6605. Springer, pp 258\u2013261. http:\/\/sourceforge.net\/projects\/gavsplus\/","DOI":"10.1007\/978-3-642-19835-9_22"},{"key":"356_CR22","doi-asserted-by":"crossref","unstructured":"de\u00a0Alfaro L (1999) Computing minimum and maximum reachability times in probabilistic systems. In: Baeten J, Mauw S (eds) Proceedings of CONCUR\u201999, LNCS, vol 1664. Springer, pp 66\u201381","DOI":"10.1007\/3-540-48320-9_7"},{"key":"356_CR23","doi-asserted-by":"crossref","unstructured":"de\u00a0Alfaro L, Henzinger T (2000) Concurrent omega-regular games. In: LICS\u201900. ACM, pp 141\u2013154","DOI":"10.1109\/LICS.2000.855763"},{"issue":"3","key":"356_CR24","doi-asserted-by":"publisher","first-page":"188","DOI":"10.1016\/j.tcs.2007.07.008","volume":"386","author":"L de Alfaro","year":"2007","unstructured":"de Alfaro L, Henzinger T, Kupferman O (2007) Concurrent reachability games. Theor Comput Sci 386(3):188\u2013217","journal-title":"Theor Comput Sci"},{"issue":"2","key":"356_CR25","doi-asserted-by":"publisher","first-page":"374","DOI":"10.1016\/j.jcss.2003.07.009","volume":"68","author":"L de Alfaro","year":"2004","unstructured":"de Alfaro L, Majumdar R (2004) Quantitative solution of omega-regular games. J Comput Syst Sci 68(2):374\u2013397","journal-title":"J Comput Syst Sci"},{"key":"356_CR26","doi-asserted-by":"crossref","unstructured":"De\u00a0Moura L, Bj\u00f8rner N (2008) Z3: an efficient SMT solver. In: Ramakrishnan C, Rehof J (eds) Proceedings of TACAS\u201908, LNCS, vol 4963. Springer, pp 337\u2013340. http:\/\/github.com\/Z3Prover\/z3","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"356_CR27","doi-asserted-by":"crossref","unstructured":"Dileepa F, Dong N, Jegourel C, Dong J (2018) Verification of strong Nash-equilibrium for probabilistic BAR systems. In: Sun J, Sun M (eds) Proceedings of ICFEM\u201918, LNCS, vol 11232. Springer, pp 106\u2013123","DOI":"10.1007\/978-3-030-02450-5_7"},{"key":"356_CR28","doi-asserted-by":"crossref","unstructured":"Dutertre B (2014) Yices 2.2. In: Biere A, Bloem R (eds) Proceedings of CAV\u201914, LNCS, vol 8559. Springer, pp 737\u2013744. http:\/\/yices.csl.sri.com","DOI":"10.1007\/978-3-319-08867-9_49"},{"key":"356_CR29","doi-asserted-by":"crossref","unstructured":"Fearnley J, Savani R (2015) The complexity of the simplex method. In: Proceedings of STOC\u201915. ACM, pp 201\u2013208","DOI":"10.1145\/2746539.2746558"},{"issue":"2","key":"356_CR30","doi-asserted-by":"publisher","first-page":"251","DOI":"10.1016\/0022-0531(83)90076-5","volume":"31","author":"D Fudenberg","year":"1983","unstructured":"Fudenberg D, Levine D (1983) Subgame-perfect equilibria of finite- and infinite-horizon games. J Econ Theory 31(2):251\u2013268","journal-title":"J Econ Theory"},{"key":"356_CR31","unstructured":"Gansner E, Koutsofios E, North S (2015) Drawing graphs with Dot. Dot User\u2019s Manual"},{"issue":"1","key":"356_CR32","doi-asserted-by":"publisher","first-page":"80","DOI":"10.1016\/0899-8256(89)90006-7","volume":"1","author":"I Gilboa","year":"1989","unstructured":"Gilboa I, Zemel E (1989) Nash and correlated equilibria: some complexity considerations. Games Econ Behav 1(1):80\u201393","journal-title":"Games Econ Behav"},{"key":"356_CR33","unstructured":"Gutierrez J, Najib M, Giuseppe P, Wooldridge M (2019) Equilibrium design for concurrent games. In: Fokkink W, van Glabbeek R (eds) Proceedings of CONCUR\u201919, LIPIcs, vol 140. Leibniz-Zentrum f\u00fcr Informatik, pp 22:1\u201322:16"},{"key":"356_CR34","doi-asserted-by":"crossref","unstructured":"Gutierrez J, Najib M, Perelli G, Wooldridge M (2018) EVE: a tool for temporal equilibrium analysis. In: Lahiri S, Wang C (eds) Proceedings of ATVA\u201918, LNCS, vol 11138. Springer, pp 551\u2013557. http:\/\/github.com\/eve-mas\/eve-parity","DOI":"10.1007\/978-3-030-01090-4_35"},{"key":"356_CR35","doi-asserted-by":"publisher","first-page":"103353","DOI":"10.1016\/j.artint.2020.103353","volume":"287","author":"J Gutierrez","year":"2020","unstructured":"Gutierrez J, Najib M, Perelli G, Wooldridge M (2020) Automated temporal equilibrium analysis: verification and synthesis of multi-player games. Artif Intell 287:103353","journal-title":"Artif Intell"},{"key":"356_CR36","doi-asserted-by":"publisher","first-page":"111","DOI":"10.1016\/j.tcs.2016.12.003","volume":"735","author":"S Haddad","year":"2018","unstructured":"Haddad S, Monmege B (2018) Interval iteration algorithm for MDPs and IMDPs. Theor Comput Sci 735:111\u2013131","journal-title":"Theor Comput Sci"},{"key":"356_CR37","doi-asserted-by":"publisher","first-page":"380","DOI":"10.1007\/s00224-013-9524-6","volume":"55","author":"K Hansen","year":"2011","unstructured":"Hansen K, Ibsen-Jensen R, Miltersen P (2011) The complexity of solving reachability games using value and strategy iteration. Theory Comput Syst 55:380\u2013403","journal-title":"Theory Comput Syst"},{"issue":"5","key":"356_CR38","doi-asserted-by":"publisher","first-page":"512","DOI":"10.1007\/BF01211866","volume":"6","author":"H Hansson","year":"1994","unstructured":"Hansson H, Jonsson B (1994) A logic for reasoning about time and reliability. Formal Asp Comput 6(5):512\u2013535","journal-title":"Formal Asp Comput"},{"key":"356_CR39","doi-asserted-by":"publisher","first-page":"246","DOI":"10.1038\/s41586-018-0277-x","volume":"559","author":"C Hilbe","year":"2018","unstructured":"Hilbe C, \u0160imsa \u0160, Chatterjee K, Nowak M (2018) Evolution of cooperation in stochastic games. Nature 559:246\u2013249","journal-title":"Nature"},{"key":"356_CR40","unstructured":"ILOG CPLEX. http:\/\/ibm.com\/products\/ilog-cplex-optimization-studio"},{"issue":"4","key":"356_CR41","doi-asserted-by":"publisher","first-page":"373","DOI":"10.1007\/BF02579150","volume":"4","author":"N Karmarkar","year":"1984","unstructured":"Karmarkar N (1984) A new polynomial-time algorithm for linear programming. Combinatorica 4(4):373\u2013395","journal-title":"Combinatorica"},{"key":"356_CR42","doi-asserted-by":"crossref","unstructured":"Kelmendi E, Kr\u00e4mer J, Kret\u00ednsk\u00fd J, Weininger M (2018) Value iteration for simple stochastic games: stopping criterion and learning algorithm. In: Chockler H, Weissenbacher G (eds) Proceedings of CAV\u201918, LNCS, vol 10981. Springer, pp 623\u2013642","DOI":"10.1007\/978-3-319-96145-3_36"},{"key":"356_CR43","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4684-9455-6","volume-title":"Denumerable Markov chains","author":"J Kemeny","year":"1976","unstructured":"Kemeny J, Snell J, Knapp A (1976) Denumerable Markov chains. Springer, Berlin"},{"key":"356_CR44","doi-asserted-by":"crossref","unstructured":"Kwiatkowska M, Norman G, Parker D (2011) PRISM 4.0: verification of probabilistic real-time systems. In: Gopalakrishnan G, Qadeer S (eds) Proceedings of CAV\u201911, LNCS, vol 6806. Springer, pp 585\u2013591. http:\/\/prismmodelchecker.org","DOI":"10.1007\/978-3-642-22110-1_47"},{"key":"356_CR45","doi-asserted-by":"crossref","unstructured":"Kwiatkowska M, Norman G, Parker D, Santos G (2018) Automated verification of concurrent stochastic games. In: Horvath A, McIver A (eds) Proceedings of QEST\u201918, LNCS, vol 11024. Springer, pp 223\u2013239","DOI":"10.1007\/978-3-319-99154-2_14"},{"key":"356_CR46","doi-asserted-by":"crossref","unstructured":"Kwiatkowska M, Norman G, Parker D, Santos G (2019) Equilibria-based probabilistic model checking for concurrent stochastic games. In: ter Beek M, McIver A, Oliveira J (eds) Proceedings of FM\u201919, LNCS, vol 11800. Springer, pp 298\u2013315","DOI":"10.1007\/978-3-030-30942-8_19"},{"key":"356_CR47","doi-asserted-by":"crossref","unstructured":"Kwiatkowska M, Norman G, Parker D, Santos G (2020) Multi-player equilibria verification for concurrent stochastic games. In: Gribaudo M, Jansen D, Remke A (eds) Proceedings of QEST\u201920, LNCS. Springer (to appear)","DOI":"10.1007\/978-3-030-59854-9_7"},{"key":"356_CR48","doi-asserted-by":"crossref","unstructured":"Kwiatkowska M, Norman G, Parker D, Santos G (2020) PRISM-games 3.0: stochastic game verification with concurrency, equilibria and time. In: Proceedings of 32nd international conference on computer aided verification (CAV\u201920), LNCS, vol 12225. Springer, pp 475\u2013487","DOI":"10.1007\/978-3-030-53291-8_25"},{"key":"356_CR49","doi-asserted-by":"crossref","unstructured":"Kwiatkowska M, Parker D (2013) Automated verification and strategy synthesis for probabilistic systems. In: Hung DV, Ogawa M (eds) Proceedings of ATVA\u201913, LNCS, vol 8172. Springer, pp 5\u201322","DOI":"10.1007\/978-3-319-02444-8_2"},{"key":"356_CR50","doi-asserted-by":"crossref","unstructured":"Kwiatkowska M, Parker D, Simaitis A (2013) Strategic analysis of trust models for user-centric networks. In: Mogavero F, Murano A, Vardi M (eds) Proceedings of SR\u201913, EPTCS, vol 112. Open Publishing Association, pp 53\u201360","DOI":"10.4204\/EPTCS.112.10"},{"issue":"2","key":"356_CR51","doi-asserted-by":"publisher","first-page":"195","DOI":"10.1007\/s10009-017-0476-z","volume":"20","author":"M Kwiatkowska","year":"2018","unstructured":"Kwiatkowska M, Parker D, Wiltsche C (2018) PRISM-games: verification and strategy synthesis for stochastic multi-player games with multiple objectives. Softw Tools Technol Transf 20(2):195\u2013210","journal-title":"Softw Tools Technol Transf"},{"issue":"2","key":"356_CR52","doi-asserted-by":"publisher","first-page":"413","DOI":"10.1137\/0112033","volume":"12","author":"C Lemke","year":"1964","unstructured":"Lemke C, Howson JJ (1964) Equilibrium points of bimatrix games. J Soc Ind Appl Math 12(2):413\u2013423","journal-title":"J Soc Ind Appl Math"},{"key":"356_CR53","doi-asserted-by":"crossref","unstructured":"Lozovanu D, Pickl S (2017) Determining Nash equilibria for stochastic positional games with discounted payoffs. In: Rothe J (ed) Proceedings of ADT\u201917, LNAI, vol 10576. Springer, pp 339\u2013343","DOI":"10.1007\/978-3-319-67504-6_24"},{"key":"356_CR54","unstructured":"LPSolve (version 5.5). http:\/\/lpsolve.sourceforge.net\/5.5\/"},{"issue":"4","key":"356_CR55","doi-asserted-by":"publisher","first-page":"1565","DOI":"10.2307\/2586667","volume":"63","author":"D Martin","year":"1998","unstructured":"Martin D (1998) The determinacy of Blackwell games. J Symb Logic 63(4):1565\u20131581","journal-title":"J Symb Logic"},{"issue":"1","key":"356_CR56","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1182613.1182616","volume":"8","author":"A McIver","year":"2007","unstructured":"McIver A, Morgan C (2007) Results on the quantitative mu-calculus qMu. ACM Trans Comput Logic 8(1):1\u201343","journal-title":"ACM Trans Comput Logic"},{"key":"356_CR57","unstructured":"McKelvey R, McLennan A, Turocy T Gambit: software tools for game theory. http:\/\/gambit-project.org"},{"key":"356_CR58","doi-asserted-by":"publisher","first-page":"48","DOI":"10.1073\/pnas.36.1.48","volume":"36","author":"J Nash","year":"1950","unstructured":"Nash J (1950) Equilibrium points in $$n$$-person games. Proc Natl Acad Sci 36:48\u201349","journal-title":"Proc Natl Acad Sci"},{"key":"356_CR59","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511800481","volume-title":"Algorithmic game theory","author":"N Nisan","year":"2007","unstructured":"Nisan N, Roughgarden T, Tardos E, Vazirani V (2007) Algorithmic game theory. Cambridge University Press, Cambridge"},{"key":"356_CR60","unstructured":"Nudelman E, Wortman J, Shoham Y, Leyton-Brown K (2004) Run the GAMUT: a comprehensive approach to evaluating game-theoretic algorithms. In: Proceedings of AAMAS\u201904. IEEE, pp 880\u2013887. http:\/\/gamut.stanford.edu"},{"key":"356_CR61","volume-title":"An introduction to game theory","author":"M Osborne","year":"2004","unstructured":"Osborne M, Rubinstein A (2004) An introduction to game theory. Oxford University Press, Oxford"},{"key":"356_CR62","doi-asserted-by":"crossref","unstructured":"Pacheco J, Santos F, Souza M, Skyrms B (2011) Evolutionary dynamics of collective action. In: The mathematics of Darwin\u2019s legacy, mathematics and biosciences in interaction. Springer, pp 119\u2013138","DOI":"10.1007\/978-3-0348-0122-5_7"},{"issue":"3","key":"356_CR63","doi-asserted-by":"publisher","first-page":"498","DOI":"10.1016\/S0022-0000(05)80063-7","volume":"48","author":"C Papadimitriou","year":"1994","unstructured":"Papadimitriou C (1994) On the complexity of the parity argument and other inefficient proofs of existence. J Comput Syst Sci 48(3):498\u2013532","journal-title":"J Comput Syst Sci"},{"key":"356_CR64","unstructured":"Porter R, Nudelman E, Shoham Y (2004) Simple search methods for finding a Nash equilibrium. In: Proceedings of AAAI\u201904. AAAI Press, pp 664\u2013669"},{"key":"356_CR65","unstructured":"Prasad H, Prashanth L, Bhatnagar S (2015) Two-timescale algorithms for learning Nash equilibria in general-sum stochastic games. In: Proceedings of AAMAS\u201915. IFAAMAS, pp 1371\u20131379"},{"key":"356_CR66","doi-asserted-by":"publisher","DOI":"10.1002\/9780470316887","volume-title":"Markov decision processes: discrete stochastic dynamic programming","author":"M Puterman","year":"1994","unstructured":"Puterman M (1994) Markov decision processes: discrete stochastic dynamic programming. Wiley, Hoboken"},{"issue":"11115","key":"356_CR67","first-page":"1","volume":"8","author":"H Qin","year":"2018","unstructured":"Qin H, Tang W, Tso R (2018) Rational quantum secret sharing. Sci Rep 8(11115):1\u20137","journal-title":"Sci Rep"},{"issue":"6","key":"356_CR68","first-page":"437","volume":"35","author":"T Raghavan","year":"1991","unstructured":"Raghavan T, Filar J (1991) Algorithms for stochastic games\u2014a survey. Z Oper Re 35(6):437\u2013472","journal-title":"Z Oper Re"},{"key":"356_CR69","unstructured":"Sandholm T, Gilpin A, Conitzer V (2005) Mixed-integer programming methods for finding Nash equilibria. In: Proceedings of AAAI\u201905. AAAI Press, pp 495\u2013501"},{"issue":"1","key":"356_CR70","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1006\/game.2000.0794","volume":"34","author":"U Schwalbe","year":"2001","unstructured":"Schwalbe U, Walker P (2001) Zermelo and the early history of game theory. Games Econ Behav 34(1):123\u2013137","journal-title":"Games Econ Behav"},{"key":"356_CR71","doi-asserted-by":"publisher","first-page":"1095","DOI":"10.1073\/pnas.39.10.1095","volume":"39","author":"L Shapley","year":"1953","unstructured":"Shapley L (1953) Stochastic games. PNAS 39:1095\u20131100","journal-title":"PNAS"},{"key":"356_CR72","doi-asserted-by":"crossref","unstructured":"Shapley L (1974) A note on the Lemke-Howson algorithm. In: Balinski M (ed) Pivoting and extension: in honor of A.W. Tucker, mathematical programming studies, vol\u00a01. Springer, pp 175\u2013189","DOI":"10.1007\/BFb0121248"},{"issue":"3","key":"356_CR73","doi-asserted-by":"publisher","first-page":"417","DOI":"10.1007\/s101070100261","volume":"91","author":"M Todd","year":"2002","unstructured":"Todd M (2002) The many facets of linear programming. Math Program 91(3):417\u2013436","journal-title":"Math Program"},{"key":"356_CR74","doi-asserted-by":"crossref","unstructured":"Toumi A, Gutierrez J, Wooldridge M (2015) A tool for the automated verification of Nash equilibria in concurrent games. In: Leucker M, Rueda C, Valencia F (eds) Proceedings of ICTAC\u201915, LNCS, vol 9399. Springer, pp 583\u2013594","DOI":"10.1007\/978-3-319-25150-9_34"},{"key":"356_CR75","doi-asserted-by":"crossref","unstructured":"Ummels M (2010) Stochastic multiplayer games: theory and algorithms. Ph.D. thesis, RWTH Aachen University","DOI":"10.5117\/9789085550402"},{"key":"356_CR76","doi-asserted-by":"publisher","first-page":"295","DOI":"10.1007\/BF01448847","volume":"100","author":"J von Neumann","year":"1928","unstructured":"von Neumann J (1928) Zur theorie der gesellschaftsspiele. Math Ann 100:295\u2013320","journal-title":"Math Ann"},{"key":"356_CR77","volume-title":"Theory of games and economic behavior","author":"J von Neumann","year":"1944","unstructured":"von Neumann J, Morgenstern O, Kuhn H, Rubinstein A (1944) Theory of games and economic behavior. Princeton University Press, Princeton"},{"key":"356_CR78","doi-asserted-by":"crossref","unstructured":"Zhu Q, Ba\u015far T (2009) Dynamic policy-based IDS configuration. In: CDC\u201909. IEEE, pp 8600\u20138605","DOI":"10.1109\/CDC.2009.5399894"},{"key":"356_CR79","doi-asserted-by":"crossref","unstructured":"Zhu Q, Li H, Han Z, Ba\u015far T (2010) A stochastic game model for jamming in multi-channel cognitive radio systems. In: Proceedings of ICC\u201910. IEEE, pp 1\u20136","DOI":"10.1109\/ICC.2010.5502451"},{"key":"356_CR80","unstructured":"PRISM-games web site. http:\/\/prismmodelchecker.org\/games\/"},{"key":"356_CR81","unstructured":"Supporting material. http:\/\/prismmodelchecker.org\/files\/fmsd-csgs\/"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-020-00356-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10703-020-00356-y\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-020-00356-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,8,26]],"date-time":"2022-08-26T15:50:07Z","timestamp":1661529007000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10703-020-00356-y"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,1,22]]},"references-count":81,"journal-issue":{"issue":"1-2","published-print":{"date-parts":[[2021,10]]}},"alternative-id":["356"],"URL":"https:\/\/doi.org\/10.1007\/s10703-020-00356-y","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,1,22]]},"assertion":[{"value":"28 February 2020","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"26 November 2020","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"22 January 2021","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}