Multi-player equilibria verification for concurrent stochastic games
From MaRDI portal
Publication:2056983
Applications of game theory (91A80) Specification and verification (program logics, model checking, etc.) (68Q60) Stochastic games, stochastic differential games (91A15) Temporal logic (03B44) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)
Abstract: Concurrent stochastic games (CSGs) are an ideal formalism for modelling probabilistic systems that feature multiple players or components with distinct objectives making concurrent, rational decisions. Examples include communication or security protocols and multi-robot navigation. Verification methods for CSGs exist but are limited to scenarios where agents or players are grouped into two coalitions, with those in the same coalition sharing an identical objective. In this paper, we propose multi-coalitional verification techniques for CSGs. We use subgame-perfect social welfare (or social cost) optimal Nash equilibria, which are strategies where there is no incentive for any coalition to unilaterally change its strategy in any game state, and where the total combined objectives are maximised (or minimised). We present an extension of the temporal logic rPATL (probabilistic alternating-time temporal logic with rewards) to specify equilibria-based properties for any number of distinct coalitions, and a corresponding model checking algorithm for a variant of stopping games. We implement our techniques in the PRISM-games tool and apply them to several case studies, including a secret sharing protocol and a public good game.
Recommendations
- Automated Verification of Concurrent Stochastic Games
- A Tool for the Automated Verification of Nash Equilibria in Concurrent Games
- Reasoning about equilibria in game-like concurrent systems
- Verification of multiplayer stochastic games via abstract dependency graphs
- Pure Nash equilibria in concurrent deterministic games
- Recursive Concurrent Stochastic Games
- Recursive Concurrent Stochastic Games
- scientific article; zbMATH DE number 7561608
- Equilibrium design for concurrent games
- Qualitative Concurrent Stochastic Games with Imperfect Information
Cited in
(10)- Reasoning about causality in games
- Stochastic games with disjunctions of multiple objectives
- Automated Verification of Concurrent Stochastic Games
- Symbolic verification and strategy synthesis for turn-based stochastic games
- A Tool for the Automated Verification of Nash Equilibria in Concurrent Games
- Correlated equilibria and fairness in concurrent stochastic games
- Equilibria-based probabilistic model checking for concurrent stochastic games
- Recursive Concurrent Stochastic Games
- Verification of multiplayer stochastic games via abstract dependency graphs
- Automatic verification of concurrent stochastic systems
This page was built for publication: Multi-player equilibria verification for concurrent stochastic games
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2056983)
