Please use this identifier to cite or link to this item: 
Year of Publication: 
[Journal:] Games [ISSN:] 2073-4336 [Volume:] 13 [Issue:] 1 [Article No.:] 19 [Publisher:] MDPI [Place:] Basel [Year:] 2022 [Pages:] 1-37
MDPI, Basel
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 ω-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 ω-regular specification in a multi-player mean-payoff game in a number of computationally relevant game-theoretic settings.
automated verification
game theory
mean-payoff games
multi-agent systems
multi-player games
temporal logic
Persistent Identifier of the first edition: 
Creative Commons License: 
cc-by Logo
Document Type: 
Appears in Collections:

Files in This Item:

Items in EconStor are protected by copyright, with all rights reserved, unless otherwise indicated.