Characterising and Verifying the Core in Concurrent Multi-Player Mean-Payoff Games

Julian Gutierrez, Anthony W. Lin, Muhammad Najib, Thomas Steeples, Michael Wooldridge

Research output: Chapter in Book/Report/Conference proceedingConference contribution

16 Downloads (Pure)


Concurrent multi-player mean-payoff games are important models for systems of agents with individual, non-dichotomous preferences. Whilst these games have been extensively studied in terms of their equilibria in non-cooperative settings, this paper explores an alternative solution concept: the core from cooperative game theory. This concept is particularly relevant for cooperative AI systems, as it enables the modelling of cooperation among agents, even when their goals are not fully aligned. Our contribution is twofold. First, we provide a characterisation of the core using discrete geometry techniques and establish a necessary and sufficient condition for its non-emptiness. We then use the characterisation to prove the existence of polynomial witnesses in the core. Second, we use the existence of such witnesses to solve key decision problems in rational verification and provide tight complexity bounds for the problem of checking whether some/every equilibrium in a game satisfies a given LTL or GR(1) specification. Our approach is general and can be adapted to handle other specifications expressed in various fragments of LTL without incurring additional computational costs.
Original languageEnglish
Title of host publication32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)
EditorsAniello Murano, Alexandra Silva
PublisherSchloss Dagstuhl - Leibniz-Zentrum für Informatik
Number of pages25
ISBN (Print)9783959773102
Publication statusPublished - 7 Feb 2024

Publication series

NameLeibniz International Proceedings in Informatics (LIPIcs)
ISSN (Print)1868-8969


  • Concurrent games
  • game theory
  • multi-agent systems
  • temporal logic

ASJC Scopus subject areas

  • Software


Dive into the research topics of 'Characterising and Verifying the Core in Concurrent Multi-Player Mean-Payoff Games'. Together they form a unique fingerprint.

Cite this