Thomas Steeples

CSL Conference 2024 Conference Paper

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

• Julian Gutierrez 0001
• Anthony W. Lin
• Muhammad Najib
• Thomas Steeples
• Michael J. Wooldridge

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.

AIJ Journal 2023 Journal Article

Cooperative concurrent games

• Julian Gutierrez
• Szymon Kowara
• Sarit Kraus
• Thomas Steeples
• Michael Wooldridge

Highlights Conference 2021 Conference Abstract

Mean-Payoff Games with omega-Regular Specifications

• Thomas Steeples

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 trying to maximise a mean-payoff function that depends on the plays so 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 this end, we consider -regular specifications, which offer a concise and intuitive way of specifying desirable behaviours of a system. The main result of our work has been the characterisation and complexity bounds for the problem of determining if there are equilibria that satisfy a given -regular specification in a multi-player mean-payoff game in a number of computationally relevant game-theoretic settings.

LAMAS&SR Workshop 2021 Workshop Paper

Mean-Payoff Games with Omega-Regular Specifications

• Thomas Steeples
• Julian Gutierrez
• Michael Wooldridge

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 trying to maximise a mean-payoff function that depends on the plays so 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 this end, we consider 𝜔-regular specifications, which offer a concise and intuitive way of specifying desirable behaviours of a system. The main results of this work are characterisation and complexity bounds for the problem of determining if there are equilibria that satisfy a given 𝜔-regular specification in a multiplayer mean-payoff game in a number of computationally relevant game-theoretic settings.

AAMAS Conference 2021 Conference Paper

Mean-Payoff Games with ω-Regular Specifications

• Thomas Steeples
• Julian Gutierrez
• Michael Wooldridge

Multi-player mean-payoff games are a natural formalism to model concurrent and multi-agent systems with self-interested players. Players in such a game traverse a graph, while trying to maximise a mean-payoff function that depends on the plays so 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 this end, we consider ω-regular specifications, which offer a concise and intuitive way of specifying desirable behaviours of a system. The main results of this work are characterisation and complexity bounds for the problem of determining if there are equilibria that satisfy a given ω-regular specification in a multi-player mean-payoff game in a number of computationally relevant game-theoretic settings.

AAMAS Conference 2018 Conference Paper

Local Equilibria in Logic-Based Multi-Player Games

• Julian Gutierrez
• Paul Harrenstein
• Thomas Steeples
• Michael Wooldridge

Game theory provides a well-established framework for the analysis and verification of concurrent and multi-agent systems. Typically, the analysis of a multi-agent system involves computing the set of equilibria in the associated multi-player game representing the behaviour of the system. As systems grow larger, it becomes increasingly harder to find equilibria in the game – which represent the rationally stable behaviours of the multi-agent system (the solutions of the game). To address this issue, in this paper, we study the concept of local equilibria, which are defined with respect to (maximal) stable coalitions of agents for which an equilibrium can de found. We focus on the solutions given by the Nash equilibria of Boolean games and iterated Boolean games, two logic-based models for multi-agent systems, in which the players’ goals are given by formulae of propositional logic and LTL, respectively.