{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,11]],"date-time":"2025-10-11T02:49:36Z","timestamp":1760150976031,"version":"build-2065373602"},"reference-count":44,"publisher":"MDPI AG","issue":"1","license":[{"start":{"date-parts":[[2022,2,9]],"date-time":"2022-02-09T00:00:00Z","timestamp":1644364800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Games"],"abstract":"<jats:p>Multi-player mean-payoff games are a natural formalism for modelling the behaviour of concurrent and multi-agent systems with self-interested players. Players in such a game traverse a graph, while attempting to maximise a (mean-)payoff function that depends on the play generated. As with all games, the equilibria that could arise may have undesirable properties. However, as system designers, we typically wish to ensure that equilibria in such systems correspond to desirable system behaviours, for example, satisfying certain safety or liveness properties. One natural way to do this would be to specify such desirable properties using temporal logic. Unfortunately, the use of temporal logic specifications causes game theoretic verification problems to have very high computational complexity. To address this issue, we consider \u03c9-regular specifications. These offer a concise and intuitive way of specifying system behaviours with a comparatively low computational overhead. The main results of this work are characterisation and complexity bounds for the problem of determining if there are equilibria that satisfy a given \u03c9-regular specification in a multi-player mean-payoff game in a number of computationally relevant game-theoretic settings.<\/jats:p>","DOI":"10.3390\/g13010019","type":"journal-article","created":{"date-parts":[[2022,2,9]],"date-time":"2022-02-09T21:19:06Z","timestamp":1644441546000},"page":"19","update-policy":"https:\/\/doi.org\/10.3390\/mdpi_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Mean-Payoff Games with \u03c9-Regular Specifications"],"prefix":"10.3390","volume":"13","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-1091-8232","authenticated-orcid":false,"given":"Julian","family":"Gutierrez","sequence":"first","affiliation":[{"name":"Monash Department of Data Science & AI, Monash Data Futures Institute, Green Chemical Futures Building, 13 Rainforest Walk, Monash University, Clayton, VIC 3800, Australia"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9328-8418","authenticated-orcid":false,"given":"Thomas","family":"Steeples","sequence":"additional","affiliation":[{"name":"Department of Computer Science, University of Oxford, Wolfson Building, Parks Road, Oxford OX1 3QD, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9329-8410","authenticated-orcid":false,"given":"Michael","family":"Wooldridge","sequence":"additional","affiliation":[{"name":"Department of Computer Science, University of Oxford, Wolfson Building, Parks Road, Oxford OX1 3QD, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"1968","published-online":{"date-parts":[[2022,2,9]]},"reference":[{"key":"ref_1","doi-asserted-by":"crossref","first-page":"672","DOI":"10.1145\/585265.585270","article-title":"Alternating-time temporal logic","volume":"49","author":"Alur","year":"2002","journal-title":"J. ACM"},{"unstructured":"Alfaro, L.d., and Henzinger, T.A. (2000, January 26\u201329). Concurrent Omega-Regular Games. Proceedings of the 15th Annual IEEE Symposium on Logic in Computer Science, Santa Barbara, CA, USA.","key":"ref_2"},{"unstructured":"Meyden, R.v.d. (2005, January 10\u201312). Games in system design and verification. Proceedings of the 10th Conference on Theoretical Aspects of Rationality and Knowledge (TARK-2005), Singapore.","key":"ref_3"},{"key":"ref_4","doi-asserted-by":"crossref","first-page":"109","DOI":"10.1007\/BF01768705","article-title":"Positional strategies for mean payoff games","volume":"8","author":"Ehrenfeucht","year":"1979","journal-title":"Int. J. Game Theory"},{"doi-asserted-by":"crossref","unstructured":"Ummels, M., and Wojtczak, D. (2011). The Complexity of Nash Equilibria in Limit-Average Games. arXiv.","key":"ref_5","DOI":"10.2168\/LMCS-7(3:20)2011"},{"key":"ref_6","doi-asserted-by":"crossref","first-page":"343","DOI":"10.1016\/0304-3975(95)00188-3","article-title":"The complexity of mean payoff games on graphs","volume":"158","author":"Zwick","year":"1996","journal-title":"Theor. Comput. Sci."},{"unstructured":"Osborne, M.J., and Rubinstein, A. (1994). A Course in Game Theory, MIT Press.","key":"ref_7"},{"key":"ref_8","doi-asserted-by":"crossref","first-page":"394","DOI":"10.1016\/j.jcss.2011.05.002","article-title":"A survey of stochastic \u03c9-regular games","volume":"78","author":"Chatterjee","year":"2012","journal-title":"J. Comput. Syst. Sci."},{"doi-asserted-by":"crossref","unstructured":"Fisman, D., Kupferman, O., and Lustig, Y. (2009). Rational Synthesis. arXiv.","key":"ref_9","DOI":"10.1007\/978-3-642-12002-2_16"},{"unstructured":"Schuurmans, D., and Wellman, M.P. (2016, January 12\u201317). Rational Verification: From Model Checking to Equilibrium Checking. Proceedings of the Thirtieth AAAI Conference on Artificial Intelligence, Phoenix, AZ, USA.","key":"ref_10"},{"unstructured":"Pnueli, A. (November, January 31). The Temporal Logic of Programs. Proceedings of the 18th Annual Symposium on Foundations of Computer Science, Providence, RI, USA.","key":"ref_11"},{"unstructured":"Clarke, E.M., and Emerson, E.A. (1981). Design and synthesis of synchronization skeletons using branching time temporal logic. Logics of Programs, Springer.","key":"ref_12"},{"key":"ref_13","first-page":"652","article-title":"On the Synthesis of an Asynchronous Reactive Module","volume":"Volume 372","author":"Ausiello","year":"1989","journal-title":"Automata, Languages and Programming, Proceedings of the 16th International Colloquium, ICALP89, Stresa, Italy, 11\u201315 July 1989"},{"key":"ref_14","doi-asserted-by":"crossref","first-page":"911","DOI":"10.1016\/j.jcss.2011.08.007","article-title":"Synthesis of Reactive(1) designs","volume":"78","author":"Bloem","year":"2012","journal-title":"J. Comput. Syst. Sci."},{"unstructured":"Kraus, S. (2019, January 10\u201316). On Computational Tractability for Rational Verification. Proceedings of the Twenty-Eighth International Joint Conference on Artificial Intelligence, IJCAI 2019, Macao, China.","key":"ref_15"},{"key":"ref_16","first-page":"479","article-title":"The Hanoi Omega-Automata Format","volume":"Volume 9206","author":"Kroening","year":"2015","journal-title":"Proceedings of the Computer Aided Verification\u201427th International Conference, CAV 2015"},{"unstructured":"Elkind, E., Veloso, M., Agmon, N., and Taylor, M.E. (2019, January 13\u201317). Cooperative Concurrent Games. Proceedings of the 18th International Conference on Autonomous Agents and MultiAgent Systems, AAMAS \u201919, Montreal, QC, Canada. Available online: http:\/\/www.cs.ox.ac.uk\/people\/michael.wooldridge\/pubs\/aamas2019.pdf.","key":"ref_17"},{"key":"ref_18","doi-asserted-by":"crossref","first-page":"123","DOI":"10.1016\/j.artint.2017.04.003","article-title":"From model checking to equilibrium checking: Reactive modules for rational verification","volume":"248","author":"Gutierrez","year":"2017","journal-title":"Artif. Intell."},{"key":"ref_19","doi-asserted-by":"crossref","first-page":"317","DOI":"10.1016\/0304-3975(91)90200-L","article-title":"On total functions, existence theorems and computational complexity","volume":"81","author":"Megiddo","year":"1991","journal-title":"Theor. Comput. Sci."},{"key":"ref_20","doi-asserted-by":"crossref","first-page":"48","DOI":"10.1073\/pnas.36.1.48","article-title":"Equilibrium points in n-person games","volume":"36","author":"Nash","year":"1950","journal-title":"Proc. Natl. Acad. Sci. USA"},{"key":"ref_21","doi-asserted-by":"crossref","first-page":"286","DOI":"10.2307\/1969529","article-title":"Non-cooperative games","volume":"54","author":"Nash","year":"1951","journal-title":"Ann. Math."},{"doi-asserted-by":"crossref","unstructured":"Tucker, A.W., and Luce, R.D. (1959). 3. Solutions to General Non-Zero-Sum Games. Contributions to the Theory of Games (AM-40), Volume IV, Princeton University Press.","key":"ref_22","DOI":"10.1515\/9781400882168"},{"doi-asserted-by":"crossref","unstructured":"Aumann, R.J. (1959). Acceptable points in general cooperative n-person games. Contributions to the Theory of Games, Volume IV, Princeton University Press. Annals of Mathematics Studies, No. 40.","key":"ref_23","DOI":"10.1515\/9781400882168-018"},{"key":"ref_24","doi-asserted-by":"crossref","first-page":"381","DOI":"10.2140\/pjm.1960.10.381","article-title":"Acceptable points in games of perfect information","volume":"10","author":"Aumann","year":"1960","journal-title":"Pac. J. Math."},{"key":"ref_25","doi-asserted-by":"crossref","first-page":"275","DOI":"10.1016\/0167-6423(87)90036-0","article-title":"Modalities for model checking: Branching time logic strikes back","volume":"8","author":"Lei","year":"1987","journal-title":"Sci. Comput. Program."},{"key":"ref_26","doi-asserted-by":"crossref","first-page":"53","DOI":"10.1016\/j.ic.2015.03.011","article-title":"Iterated Boolean games","volume":"242","author":"Gutierrez","year":"2015","journal-title":"Inf. Comput."},{"key":"ref_27","doi-asserted-by":"crossref","first-page":"309","DOI":"10.1016\/0012-365X(78)90011-0","article-title":"A characterization of the minimum cycle mean in a digraph","volume":"23","author":"Karp","year":"1978","journal-title":"Discret. Math."},{"unstructured":"Garey, M.R., and Johnson, D.S. (1979). Computers and Intractability: A Guide to the Theory of NP-Completeness, W. H. Freeman.","key":"ref_28"},{"unstructured":"Miller, R.E., and Thatcher, J.W. (1972, January 20\u201322). Reducibility among Combinatorial Problems. Proceedings of the a Symposium on the Complexity of Computer Computations, Yorktown Heights, NY, USA. The IBM Research Symposia Series.","key":"ref_29"},{"doi-asserted-by":"crossref","unstructured":"Gutierrez, J., Murano, A., Perelli, G., Rubin, S., and Wooldridge, M. (2017, January 19\u201325). Nash Equilibria in Concurrent Games with Lexicographic Preferences. Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence, IJCAI-17, Melbourne, Australia.","key":"ref_30","DOI":"10.24963\/ijcai.2017\/148"},{"key":"ref_31","doi-asserted-by":"crossref","first-page":"585","DOI":"10.1007\/s00236-020-00385-4","article-title":"Equilibria for games with combined qualitative and quantitative objectives","volume":"58","author":"Gutierrez","year":"2020","journal-title":"Acta Inform."},{"key":"ref_32","doi-asserted-by":"crossref","first-page":"177","DOI":"10.1016\/j.ic.2015.03.001","article-title":"The complexity of multi-mean-payoff and multi-energy games","volume":"241","author":"Velner","year":"2015","journal-title":"Inf. Comput."},{"key":"ref_33","first-page":"336","article-title":"Half-Positional Determinacy of Infinite Games","volume":"Volume 4052","author":"Bugliesi","year":"2006","journal-title":"Automata, Languages and Programming, Proceedings of the 33rd International Colloquium, ICALP 2006, Venice, Italy, 10\u201314 July 2006"},{"key":"ref_34","doi-asserted-by":"crossref","first-page":"733","DOI":"10.1145\/3828.3837","article-title":"The Complexity of Propositional Linear Temporal Logics","volume":"32","author":"Sistla","year":"1985","journal-title":"J. ACM"},{"key":"ref_35","first-page":"251","article-title":"Pareto Curves of Multidimensional Mean-Payoff Games","volume":"Volume 9207","author":"Kroening","year":"2015","journal-title":"Computer Aided Verification, Proceedings of the 27th International Conference, CAV 2015, San Francisco, CA, USA, 18\u201324 July 2015"},{"key":"ref_36","first-page":"50","article-title":"The core of an N person game","volume":"35","author":"Scarf","year":"1967","journal-title":"Econom. J. Econom. Soc."},{"key":"ref_37","doi-asserted-by":"crossref","first-page":"567","DOI":"10.1137\/0118049","article-title":"Some theorems on the core of an n-game without side-payments","volume":"18","author":"Billera","year":"1970","journal-title":"SIAM J. Appl. Math."},{"doi-asserted-by":"crossref","unstructured":"Shapley, L.S. (1973). On Balanced Games without Side Payments. Mathematical Programming, Elsevier.","key":"ref_38","DOI":"10.1016\/B978-0-12-358350-5.50012-9"},{"key":"ref_39","first-page":"119","article-title":"Some applications of the methods of linear programming to the theory of cooperative games","volume":"10","author":"Bondareva","year":"1963","journal-title":"Probl. Kibernet."},{"key":"ref_40","doi-asserted-by":"crossref","first-page":"453","DOI":"10.1002\/nav.3800140404","article-title":"On balanced sets and cores","volume":"14","author":"Shapley","year":"1967","journal-title":"Nav. Res. Logist. Q."},{"unstructured":"Alur, R., and Henzinger, T.A. (1996, January 27\u201330). Reactive Modules. Proceedings of the 11th Annual IEEE Symposium on Logic in Computer Science, New Brunswick, NJ, USA.","key":"ref_41"},{"unstructured":"Nakashima, H., Wellman, M.P., Weiss, G., and Stone, P. (2006, January 8\u201312). On the complexity of practical ATL model checking. Proceedings of the 5th International Joint Conference on Autonomous Agents and Multiagent Systems (AAMAS 2006), Hakodate, Japan.","key":"ref_42"},{"key":"ref_43","doi-asserted-by":"crossref","first-page":"151","DOI":"10.1137\/0208013","article-title":"Provably Difficult Combinatorial Games","volume":"8","author":"Stockmeyer","year":"1979","journal-title":"SIAM J. Comput."},{"unstructured":"Chatterjee, K., Henzinger, T.A., and Jurdzinski, M. (2005, January 26\u201329). Mean-payoff parity games. Proceedings of the 20th Annual IEEE Symposium on Logic in Computer Science (LICS\u201905), Chicago, IL, USA.","key":"ref_44"}],"container-title":["Games"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.mdpi.com\/2073-4336\/13\/1\/19\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,10]],"date-time":"2025-10-10T22:17:18Z","timestamp":1760134638000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.mdpi.com\/2073-4336\/13\/1\/19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,2,9]]},"references-count":44,"journal-issue":{"issue":"1","published-online":{"date-parts":[[2022,2]]}},"alternative-id":["g13010019"],"URL":"https:\/\/doi.org\/10.3390\/g13010019","relation":{},"ISSN":["2073-4336"],"issn-type":[{"type":"electronic","value":"2073-4336"}],"subject":[],"published":{"date-parts":[[2022,2,9]]}}}