{"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":1776333534718,"version":"3.51.2"},"publisher-location":"Cham","reference-count":40,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030995263","type":"print"},{"value":"9783030995270","type":"electronic"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2022,3,30]],"date-time":"2022-03-30T00:00:00Z","timestamp":1648598400000},"content-version":"vor","delay-in-days":88,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>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 (<jats:inline-formula><jats:alternatives><jats:tex-math>$$\\varepsilon $$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mi>\u03b5<\/mml:mi>\n                <\/mml:math><\/jats:alternatives><\/jats:inline-formula>-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 <jats:italic>correlated equilibria<\/jats:italic>, in which players can coordinate through public signals, and introduce a novel optimality criterion of <jats:italic>social fairness<\/jats:italic>, 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.<\/jats:p>","DOI":"10.1007\/978-3-030-99527-0_4","type":"book-chapter","created":{"date-parts":[[2022,3,29]],"date-time":"2022-03-29T06:37:21Z","timestamp":1648535841000},"page":"60-78","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["Correlated Equilibria and Fairness in Concurrent 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":[[2022,3,30]]},"reference":[{"key":"4_CR1","unstructured":"de Alfaro, L.: Formal Verification of Probabilistic Systems. Ph.D. thesis, Stanford University (1997)"},{"key":"4_CR2","doi-asserted-by":"crossref","unstructured":"Aminof, B., Kwiatkowska, M., B. Maubert, B., Murano, A., Rubin, S.: Probabilistic strategy logic. In: Proc. IJCAI\u201919. pp. 32\u201338 (2019)","DOI":"10.24963\/ijcai.2019\/5"},{"key":"4_CR3","doi-asserted-by":"crossref","unstructured":"Aumann, R.: Subjectivity and correlation in randomized strategies. Journal of Mathematical Economics 1(1), 67\u201396 (1974)","DOI":"10.1016\/0304-4068(74)90037-8"},{"key":"4_CR4","unstructured":"Baier, C., Katoen, J.P.: Principles of Model Checking. MIT Press (2008)"},{"key":"4_CR5","doi-asserted-by":"crossref","unstructured":"Baier, C., Kwiatkowska, M.: Model checking for a probabilistic branching time logic with fairness. Distributed Computing 11(3), 125\u2013155 (1998)","DOI":"10.1007\/s004460050046"},{"key":"4_CR6","unstructured":"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)"},{"key":"4_CR7","doi-asserted-by":"crossref","unstructured":"Brenguier, R.: PRALINE: A tool for computing Nash equilibria in concurrent games. In: Sharygina, N., Veith, H. (eds.) Proc. CAV\u201913. LNCS, vol. 8044, pp. 890\u2013895. Springer (2013), lsv.fr\/Software\/praline\/","DOI":"10.1007\/978-3-642-39799-8_63"},{"key":"4_CR8","doi-asserted-by":"crossref","unstructured":"Chatterjee, K., Fijalkow, N.: A reduction from parity games to simple stochastic games. EPTCS 54, 74\u201386 (2011)","DOI":"10.4204\/EPTCS.54.6"},{"key":"4_CR9","doi-asserted-by":"crossref","unstructured":"Chatterjee, K., Henzinger, T.: Value iteration. In: 25 Years of Model Checking. LNCS, vol. 5000, pp. 107\u2013138. Springer (2008)","DOI":"10.1007\/978-3-540-69850-0_7"},{"key":"4_CR10","doi-asserted-by":"crossref","unstructured":"Chen, T., Forejt, V., Kwiatkowska, M., Parker, D., Simaitis, A.: Automatic verification of competitive stochastic systems. Formal Methods in System Design 43(1), 61\u201392 (2013)","DOI":"10.1007\/s10703-013-0183-7"},{"key":"4_CR11","doi-asserted-by":"crossref","unstructured":"Chen, X., Deng, X., Teng, S.H.: Settling the complexity of computing two-player Nash equilibria. J. ACM 56(3) (2009)","DOI":"10.1145\/1516512.1516516"},{"key":"4_CR12","doi-asserted-by":"crossref","unstructured":"Daskalakis, C., Goldberg, P., Papadimitriou, C.: The complexity of computing a Nash equilibrium. Communications of the ACM 52(2), 89\u201397 (2009)","DOI":"10.1145\/1461928.1461951"},{"key":"4_CR13","doi-asserted-by":"crossref","unstructured":"De Moura, L., Bj\u00f8rner, N.: Z3: An efficient SMT solver. In: Proc. TACAS\u201908. LNCS, vol. 4963, pp. 337\u2013340. Springer (2008), github.com\/Z3Prover\/z3","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"4_CR14","doi-asserted-by":"crossref","unstructured":"Dutertre, B.: Yices 2.2. In: Biere, A., Bloem, R. (eds.) Proc CAV\u201914. LNCS, vol. 8559, pp. 737\u2013744. Springer (2014), yices.csl.sri.com","DOI":"10.1007\/978-3-319-08867-9_49"},{"key":"4_CR15","doi-asserted-by":"crossref","unstructured":"Gilboa, I., Zemel, E.: Nash and correlated equilibria: Some complexity considerations. Games and Economic Behavior 1(1), 80\u201393 (1989)","DOI":"10.1016\/0899-8256(89)90006-7"},{"key":"4_CR16","doi-asserted-by":"crossref","unstructured":"Griva, I., Nash, S., Sofer, A.: Linear and Nonlinear Optimization: Second Edition. CUP (01 2009)","DOI":"10.1137\/1.9780898717730"},{"key":"4_CR17","unstructured":"Gurobi Optimization, LLC: Gurobi Optimizer Reference Manual (2021), www.gurobi.com"},{"key":"4_CR18","unstructured":"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\u201914) (2014)"},{"key":"4_CR19","doi-asserted-by":"crossref","unstructured":"Hauser, O., Hilbe, C., Chatterjee, K., Nowak, M.: Social dilemmas among unequals. Nature 572, 524\u2013527 (2019)","DOI":"10.1038\/s41586-019-1488-5"},{"key":"4_CR20","doi-asserted-by":"crossref","unstructured":"Kemeny, J., Snell, J., Knapp, A.: Denumerable Markov Chains. Springer (1976)","DOI":"10.1007\/978-1-4684-9455-6"},{"key":"4_CR21","doi-asserted-by":"crossref","unstructured":"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\u201920. LNCS, Springer (2020)","DOI":"10.1007\/978-3-030-59854-9_7"},{"key":"4_CR22","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: Proc. CAV\u201920. pp. 475\u2013487. LNCS, Springer (2020)","DOI":"10.1007\/978-3-030-53291-8_25"},{"key":"4_CR23","doi-asserted-by":"crossref","unstructured":"Kwiatkowska, M., Norman, G., Parker, D., Santos, G.: Correlated equilibria and fairness in concurrent stochastic games (2022), arXiv:2201.09702","DOI":"10.1007\/978-3-030-99527-0_4"},{"key":"4_CR24","doi-asserted-by":"crossref","unstructured":"Kwiatkowska, M., Norman, G., Parker, D., Santos, G.: Automatic verification of concurrent stochastic systems. Formal Methods in System Design pp. 1\u201363 (2021)","DOI":"10.1007\/s10703-020-00356-y"},{"key":"4_CR25","unstructured":"Littman, M., Ravi, N., Talwar, A., Zinkevich, M.: An efficient optimal-equilibrium algorithm for two-player game trees. In: Proc. UAI\u201906. pp. 298\u2013305. AUAI Press (2006)"},{"key":"4_CR26","doi-asserted-by":"crossref","unstructured":"McIver, A., Morgan, C.: Results on the quantitative mu-calculus qMu. ACM Trans. Computational Logic 8(1) (2007)","DOI":"10.1145\/1182613.1182616"},{"key":"4_CR27","unstructured":"von Neumann, J., Morgenstern, O., Kuhn, H., Rubinstein, A.: Theory of Games and Economic Behavior. Princeton University Press (1944)"},{"key":"4_CR28","doi-asserted-by":"crossref","unstructured":"Nisan, N., Roughgarden, T., Tardos, E., Vazirani, V.: Algorithmic Game Theory. CUP (2007)","DOI":"10.1017\/CBO9780511800481"},{"key":"4_CR29","unstructured":"Nudelman, E., Wortman, J., Shoham, Y., Leyton-Brown, K.: Run the GAMUT: A comprehensive approach to evaluating game-theoretic algorithms. In: Proc. AAMAS\u201904. pp. 880\u2013887. ACM (2004), gamut.stanford.edu"},{"key":"4_CR30","unstructured":"Osborne, M., Rubinstein, A.: An Introduction to Game Theory. OUP (2004)"},{"key":"4_CR31","unstructured":"Porter, R., Nudelman, E., Shoham, Y.: Simple search methods for finding a Nash equilibrium. In: Proc. AAAI\u201904. pp. 664\u2013669. AAAI Press (2004)"},{"key":"4_CR32","doi-asserted-by":"crossref","unstructured":"Prisner, E.: Game Theory Through Examples. Mathematical Association of America, 1 edn. (2014)","DOI":"10.5948\/9781614441151"},{"key":"4_CR33","unstructured":"Rabin, M.: Incorporating fairness into game theory and economics. The American Economic Review 83(5), 1281\u20131302 (1993)"},{"key":"4_CR34","unstructured":"Rabin, M.: Fairness in repeated games. working paper 97\u2013252, University of California at Berkeley (1997)"},{"key":"4_CR35","doi-asserted-by":"crossref","unstructured":"Schwalbe, U., Walker, P.: Zermelo and the early history of game theory. Games and Economic Behavior 34(1), 123\u2013137 (2001)","DOI":"10.1006\/game.2000.0794"},{"key":"4_CR36","doi-asserted-by":"crossref","unstructured":"Shapley, L.: Stochastic games. PNAS 39, 1095\u20131100 (1953)","DOI":"10.1073\/pnas.39.10.1095"},{"key":"4_CR37","doi-asserted-by":"crossref","unstructured":"Stevens, S., Palocsay, S.: Teaching use of binary variables in integer linear programs: Formulating logical conditions. INFORMS Transactions on Education 18(1), 28\u201336 (2017)","DOI":"10.1287\/ited.2017.0177"},{"key":"4_CR38","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), github.com\/coin-or\/Ipopt"},{"key":"4_CR39","doi-asserted-by":"crossref","unstructured":"W\u00e4chter, A., Biegler, L.: On the implementation of an interior-point filter line-search algorithm for large-scale nonlinear programming. Mathematical Programming 106(1), 25\u201357 (2006)","DOI":"10.1007\/s10107-004-0559-y"},{"key":"4_CR40","unstructured":"Supporting material, www.prismmodelchecker.org\/files\/tacas22equ\/"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-99527-0_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,3,12]],"date-time":"2024-03-12T08:46:02Z","timestamp":1710233162000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-99527-0_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783030995263","9783030995270"],"references-count":40,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-99527-0_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"30 March 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TACAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Munich","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Germany","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2022","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2 April 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"7 April 2022","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2022","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2022\/tacas","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":"159","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":"46","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":"4","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","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":"10","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)"}},{"value":"16 tool papers of the affiliated competition SV-Comp and 1 paper consisting of the competition report are also included in the proceedings","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}