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)

Abstract

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
Pages32:1-32:25
Number of pages25
ISBN (Print)9783959773102
DOIs
Publication statusPublished - 7 Feb 2024

Publication series

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

Keywords

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

ASJC Scopus subject areas

  • Software

Fingerprint

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