Multi-player equilibria verification for concurrent stochastic games

DOI10.1007/978-3-030-59854-9_7zbMATH Open1483.68197arXiv2007.03365OpenAlexW3109427444WikidataQ112268301 ScholiaQ112268301MaRDI QIDQ2056983FDOQ2056983

Authors: Yanyan Li 

Publication date: 8 December 2021

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.

Full work available at URL: https://arxiv.org/abs/2007.03365

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

Mathematics Subject Classification ID

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)

Cited In (10)

• 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
• Automatic verification of concurrent stochastic systems
• Stochastic games with disjunctions of multiple objectives
• Recursive Concurrent Stochastic Games
• Verification of multiplayer stochastic games via abstract dependency graphs
• Reasoning about causality in games
• Correlated equilibria and fairness in concurrent stochastic games
• Equilibria-based probabilistic model checking for concurrent stochastic games

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)