Team strategies without shared randomness have distinct complexity limits
Limit-sure Winning in Team Games without Shared Randomness
Computer Science and Game TheoryFormal Languages and Automata TheoryMultiagent Systems
Summary
The paper looks at games where a team tries to achieve goals while playing against an opponent, but the team members can only use their own random choices, not a shared one. The researchers find that for games where the team wants to reach a goal, it's tough (NP-complete) to decide if they can almost always win. For games focused on avoiding bad outcomes, this decision is easier (in P). They also link these findings to the difficulty of checking certain logical properties about such games.
What this means in practice
- •For automated verification engineers: Decide the complexity of verifying if distributed systems without shared randomness meet safety goals almost always.
- •For distributed system architects: Understand when teams of agents with private randomness can guarantee reaching certain states with near certainty.
A theory result. No direct application yet.
Authors
Léonard Brice, Thomas A. Henzinger, Alipasha Montaseri, Ali Shafiee, K. S. Thejaswini
Abstract
We study concurrent stochastic games in which a team of agents plays against an adversarial environment. If the agents could access a shared source of randomness, then these games reduce to two-player games. Despite being common in the literature on coalition games, this assumption does not accurately model real-world systems. In this paper, we consider the setting where the agents only have access to individual sources of randomness, and must satisfy a given reachability or safety objective. The limit-sure problem asks whether the team can ensure that the objective is satisfied with probability at least $1-λ$ for every $λ>0$. For reachability objectives, we show that this problem is $\mathsf{NP}$-complete. For safety objectives, we show that limit-sure winning coincides with almost-sure winning, which is known to lie in $\mathsf{P}$. As a corollary of these results, we conclude that model checking of the qualitative fragment of the logic Individually Randomised ATL -- introduced in the recent work of Brice et al. -- is $\mathsf{P}^{\mathsf{NP}}$-complete.