Randomise Alone, Reach as a Team

TL;DR

It is shown that memoryless strategies are sufficient for the threshold problem (deciding whether there is a strategy for the team that ensures winning with probability that exceeds a threshold), a result that places the problem in the Existential Theory of the Reals (\exists\mathbb{R}) but also enables the construction of value iteration algorithms.

Abstract

We study concurrent graph games where n players cooperate against an opponent to reach a set of target states. Unlike traditional settings, we study distributed randomisation: team players do not share a source of randomness, and their private random sources are hidden from the opponent and from each other. We show that memoryless strategies are sufficient for the threshold problem (deciding whether there is a strategy for the team that ensures winning with probability that exceeds a threshold), a result that not only places the problem in the Existential Theory of the Reals (\exists\mathbb{R}) but also enables the construction of value iteration algorithms. We additionally show that the threshold problem is NP-hard. For the almost-sure reachability problem, we prove NP-completeness. We introduce Individually Randomised Alternating-time Temporal Logic (IRATL). This logic extends the standard ATL framework to reason about probability thresholds, with semantics explicitly designed for coalitions that lack a shared source of randomness. On the practical side, we implement and evaluate a solver for the threshold and almost-sure problem based on the algorithms that we develop.

Figures (7)

• Figure 1: The two agents choose among actions $\{L,R\}$ and the environment chooses among actions $\{L,R\}$
• Figure 2: An example game for opponent with no memory.
• Figure 3: Execution time of the algorithms across three benchmarks. The plots report execution time in seconds vs. the state space size: both in log scale.
• Figure 4: The plot compares the execution time (in seconds, logarithmic scale) of SAT-Direct under individual and shared randomness constraints against the baseline qualitative solver (which assumes shared randomness)
• Figure 5: Visualizations of the six scenarios used for evaluation. Scenarios 1--4 involve two team players. Scenarios 5 and 6 involve three team players. Green nodes indicate the team's starting positions, while the red node indicates the opponent's. The results are available in Table \ref{['table:graphgame']}.

Theorems & Definitions (61)

• definition 1: Game structure, game
• lemma 1: App. \ref{['app:VIconvergencetovalue']}
• theorem 1: App. \ref{['app:memmless-optimal']}
• proof : sketch
• theorem 2: App. \ref{['app:memlessOpp']}
• proof : sketch
• theorem 3: App. \ref{['app:ETRComplete']}
• proof : sketch
• theorem 4: App. \ref{['app:NPhardnessThreshold']}
• proof : sketch