{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T09:58:20Z","timestamp":1776333500874,"version":"3.51.2"},"publisher-location":"Cham","reference-count":41,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030598532","type":"print"},{"value":"9783030598549","type":"electronic"}],"license":[{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2020]]},"DOI":"10.1007\/978-3-030-59854-9_7","type":"book-chapter","created":{"date-parts":[[2020,11,2]],"date-time":"2020-11-02T23:02:42Z","timestamp":1604358162000},"page":"74-95","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":8,"title":["Multi-player Equilibria Verification for\u00a0Concurrent Stochastic Games"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9022-7599","authenticated-orcid":false,"given":"Marta","family":"Kwiatkowska","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9326-4344","authenticated-orcid":false,"given":"Gethin","family":"Norman","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4137-8862","authenticated-orcid":false,"given":"David","family":"Parker","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6570-9737","authenticated-orcid":false,"given":"Gabriel","family":"Santos","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2020,11,3]]},"reference":[{"key":"7_CR1","unstructured":"de Alfaro, L.: Formal verification of probabilistic systems. Ph.D. thesis, Stanford University (1997)"},{"issue":"3","key":"7_CR2","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.: Concurrent reachability games. Theoret. Comput. Sci. 386(3), 188\u2013217 (2007)","journal-title":"Theoret. Comput. Sci."},{"issue":"2","key":"7_CR3","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.: Quantitative solution of omega-regular games. J. Comput. Syst. Sci. 68(2), 374\u2013397 (2004)","journal-title":"J. Comput. Syst. Sci."},{"issue":"5","key":"7_CR4","doi-asserted-by":"publisher","first-page":"672","DOI":"10.1145\/585265.585270","volume":"49","author":"R Alur","year":"2002","unstructured":"Alur, R., Henzinger, T.A., Kupferman, O.: Alternating-time temporal logic. J. ACM 49(5), 672\u2013713 (2002)","journal-title":"J. ACM"},{"issue":"1","key":"7_CR5","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1016\/0304-4068(74)90037-8","volume":"1","author":"R Aumann","year":"1974","unstructured":"Aumann, R.: Subjectivity and correlation in randomized strategies. J. Math. Econ. 1(1), 67\u201396 (1974)","journal-title":"J. Math. Econ."},{"key":"7_CR6","unstructured":"Bouyer, P., Markey, N., Stan, D.: Mixed Nash equilibria in concurrent games. In: Proceedings of FSTTCS 2014, LIPICS, vol. 29, pp. 351\u2013363. Leibniz-Zentrum f\u00fcr Informatik (2014)"},{"key":"7_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"890","DOI":"10.1007\/978-3-642-39799-8_63","volume-title":"Computer Aided Verification","author":"R Brenguier","year":"2013","unstructured":"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\u2013895. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_63"},{"key":"7_CR8","unstructured":"Brihaye, T., Bruy\u00e8re, 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\u201313:16. Leibniz-Zentrum f\u00fcr Informatik (2019)"},{"key":"7_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"525","DOI":"10.1007\/978-3-319-08867-9_34","volume-title":"Computer Aided Verification","author":"P \u010cerm\u00e1k","year":"2014","unstructured":"\u010cerm\u00e1k, 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\u2013532. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_34"},{"issue":"5","key":"7_CR10","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.: Strategy improvement for concurrent reachability and turn-based stochastic safety games. J. Comput. Syst. Sci. 79(5), 640\u2013657 (2013)","journal-title":"J. Comput. Syst. Sci."},{"key":"7_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1007\/978-3-540-69850-0_7","volume-title":"25 Years of Model Checking","author":"K Chatterjee","year":"2008","unstructured":"Chatterjee, K., Henzinger, T.A.: Value iteration. In: Grumberg, O., Veith, H. (eds.) 25 Years of Model Checking. LNCS, vol. 5000, pp. 107\u2013138. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-69850-0_7"},{"issue":"1","key":"7_CR12","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.: Automatic verification of competitive stochastic systems. Formal Methods Syst. Design 43(1), 61\u201392 (2013)","journal-title":"Formal Methods Syst. Design"},{"key":"7_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"266","DOI":"10.1007\/978-3-642-40313-2_25","volume-title":"Mathematical Foundations of Computer Science 2013","author":"T Chen","year":"2013","unstructured":"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\u2013277. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-40313-2_25"},{"key":"7_CR14","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1145\/1345037.1345039","volume":"7","author":"P Cramton","year":"2007","unstructured":"Cramton, P., Shoham, Y., Steinberg, R.: An overview of combinatorial auctions. SIGecom Exchanges 7, 3\u201314 (2007)","journal-title":"SIGecom Exchanges"},{"issue":"2","key":"7_CR15","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1145\/1461928.1461951","volume":"52","author":"C Daskalakis","year":"2009","unstructured":"Daskalakis, C., Goldberg, P., Papadimitriou, C.: The complexity of computing a Nash equilibrium. Commun. ACM 52(2), 89\u201397 (2009)","journal-title":"Commun. ACM"},{"key":"7_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L de Moura","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"issue":"1","key":"7_CR17","doi-asserted-by":"publisher","first-page":"65","DOI":"10.1016\/S0022-0531(03)00005-X","volume":"110","author":"S Govindan","year":"2003","unstructured":"Govindan, S., Wilson, R.: A global newton method to compute Nash equilibria. J. Econ. Theory 110(1), 65\u201386 (2003)","journal-title":"J. Econ. Theory"},{"key":"7_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"551","DOI":"10.1007\/978-3-030-01090-4_35","volume-title":"Automated Technology for Verification and Analysis","author":"J Gutierrez","year":"2018","unstructured":"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\u2013557. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-030-01090-4_35"},{"key":"7_CR19","doi-asserted-by":"crossref","unstructured":"Halpern, J., Teague, V.: Rational secret sharing and multiparty computation: extended abstract. In: Proceedings of STOC 2004, pp. 623\u2013632. ACM (2004)","DOI":"10.1145\/1007352.1007447"},{"key":"7_CR20","doi-asserted-by":"publisher","first-page":"524","DOI":"10.1038\/s41586-019-1488-5","volume":"572","author":"O Hauser","year":"2019","unstructured":"Hauser, O., Hilbe, C., Chatterjee, K., Nowak, M.: Social dilemmas among unequals. Nature 572, 524\u2013527 (2019)","journal-title":"Nature"},{"key":"7_CR21","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.: Denumerable Markov Chains. Springer, New York (1976). https:\/\/doi.org\/10.1007\/978-1-4684-9455-6"},{"key":"7_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1007\/978-3-319-99154-2_14","volume-title":"Quantitative Evaluation of Systems","author":"M Kwiatkowska","year":"2018","unstructured":"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\u2013239. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-99154-2_14"},{"key":"7_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"298","DOI":"10.1007\/978-3-030-30942-8_19","volume-title":"Formal Methods \u2013 The Next 30 Years","author":"M Kwiatkowska","year":"2019","unstructured":"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\u2013315. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-30942-8_19"},{"key":"7_CR24","unstructured":"Kwiatkowska, M., Norman, G., Parker, D., Santos, G.: Multi-player equilibria verification for concurrent stochastic games (2020). arXiv:2007.03365"},{"key":"7_CR25","doi-asserted-by":"crossref","unstructured":"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","DOI":"10.1007\/978-3-030-53291-8_25"},{"key":"7_CR26","unstructured":"McKelvey, R., McLennan, A., Turocy, T.: Gambit: software tools for game theory, version 16.0.1 (2016). http:\/\/www.gambit-project.org"},{"key":"7_CR27","doi-asserted-by":"publisher","unstructured":"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\u2013131. Springer, London (2009). https:\/\/doi.org\/10.1007\/978-1-84800-938-7_2","DOI":"10.1007\/978-1-84800-938-7_2"},{"key":"7_CR28","volume-title":"Theory of Games and Economic Behavior","author":"J von Neumann","year":"1944","unstructured":"von Neumann, J., Morgenstern, O., Kuhn, H., Rubinstein, A.: Theory of Games and Economic Behavior. Princeton University Press, Princeton (1944)"},{"key":"7_CR29","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.: Algorithmic Game Theory. CUP, Cambridge (2007)"},{"issue":"4","key":"7_CR30","doi-asserted-by":"publisher","first-page":"1674","DOI":"10.1137\/060649513","volume":"19","author":"J Nocedal","year":"2009","unstructured":"Nocedal, J., W\u00e4chter, A., Waltz, R.: Adaptive barrier update strategies for nonlinear interior methods. SIAM J. Optim. 19(4), 1674\u20131693 (2009)","journal-title":"SIAM J. Optim."},{"key":"7_CR31","unstructured":"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\u2013887. ACM (2004). http:\/\/www.gamut.stanford.edu"},{"key":"7_CR32","volume-title":"An Introduction to Game Theory","author":"M Osborne","year":"2004","unstructured":"Osborne, M., Rubinstein, A.: An Introduction to Game Theory. OUP, Oxford (2004)"},{"key":"7_CR33","unstructured":"Porter, R., Nudelman, E., Shoham, Y.: Simple search methods for finding a Nash equilibrium. In: Proceedings of AAAI 2004, pp. 664\u2013669. AAAI Press (2004)"},{"key":"7_CR34","doi-asserted-by":"publisher","first-page":"236","DOI":"10.1145\/506147.506153","volume":"49","author":"T Roughgarden","year":"2002","unstructured":"Roughgarden, T., Tardos, E.: How bad is selfish routing? J. ACM 49, 236\u2013259 (2002)","journal-title":"J. ACM"},{"issue":"1","key":"7_CR35","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.: Zermelo and the early history of game theory. Games Econ. Behav. 34(1), 123\u2013137 (2001)","journal-title":"Games Econ. Behav."},{"key":"7_CR36","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1006\/jeth.1997.2460","volume":"83","author":"M Shimoji","year":"1998","unstructured":"Shimoji, M., Watson, J.: Conditional dominance, rationalizability, and game forms. J. Econ. Theory 83, 161\u2013195 (1998)","journal-title":"J. Econ. Theory"},{"key":"7_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"583","DOI":"10.1007\/978-3-319-25150-9_34","volume-title":"Theoretical Aspects of Computing \u2013 ICTAC 2015","author":"A Toumi","year":"2015","unstructured":"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\u2013594. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-25150-9_34"},{"issue":"3","key":"7_CR38","doi-asserted-by":"publisher","first-page":"377","DOI":"10.1287\/moor.12.3.377","volume":"12","author":"G Van Der Laan","year":"1987","unstructured":"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\u2013397 (1987)","journal-title":"Math. Oper. Res."},{"key":"7_CR39","unstructured":"W\u00e4chter, A.: Short tutorial: getting started with IPOPT in 90 minutes. In: Combinatorial Scientific Computing, no. 09061 in Dagstuhl Seminar Proceedings. Leibniz-Zentrum f\u00fcr Informatik (2009). http:\/\/www.github.com\/coin-or\/Ipopt"},{"issue":"1","key":"7_CR40","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1007\/s10107-004-0559-y","volume":"106","author":"A W\u00e4chter","year":"2006","unstructured":"W\u00e4chter, A., Biegler, L.: On the implementation of an interior-point filter line-search algorithm for large-scale nonlinear programming. Math. Program. 106(1), 25\u201357 (2006)","journal-title":"Math. Program."},{"key":"7_CR41","unstructured":"Supporting material. http:\/\/www.prismmodelchecker.org\/files\/qest20"}],"container-title":["Lecture Notes in Computer Science","Quantitative Evaluation of Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-59854-9_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,12,17]],"date-time":"2020-12-17T16:12:26Z","timestamp":1608221546000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-59854-9_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030598532","9783030598549"],"references-count":41,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-59854-9_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020]]},"assertion":[{"value":"3 November 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"QEST","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Quantitative Evaluation of Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Vienna","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Austria","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2020","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"31 August 2020","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"3 September 2020","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"17","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"qest2020","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/www.qest.org\/qest2020\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"easychair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"42","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"12","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"7","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"29% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3,10","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"4,06","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}