Bitte verwenden Sie diesen Link, um diese Publikation zu zitieren, oder auf sie als Internetquelle zu verweisen: https://hdl.handle.net/10419/257595 
Erscheinungsjahr: 
2022
Quellenangabe: 
[Journal:] Games [ISSN:] 2073-4336 [Volume:] 13 [Issue:] 1 [Article No.:] 19 [Publisher:] MDPI [Place:] Basel [Year:] 2022 [Pages:] 1-37
Verlag: 
MDPI, Basel
Zusammenfassung: 
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.
Schlagwörter: 
automated verification
equilibria
game theory
mean-payoff games
multi-agent systems
multi-player games
temporal logic
Persistent Identifier der Erstveröffentlichung: 
Creative-Commons-Lizenz: 
cc-by Logo
Dokumentart: 
Article
Erscheint in der Sammlung:

Datei(en):
Datei
Größe





Publikationen in EconStor sind urheberrechtlich geschützt.