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.

翻译：我们研究了n个玩家在并发博弈图中合作对抗一名对手以到达一组目标状态的问题。与传统设定不同，我们聚焦于分布式随机化：团队成员不共享随机源，且其私有随机源对对手和彼此均不可见。我们证明，无记忆策略足以解决阈值问题（判断是否存在使团队获胜概率超过给定阈值的策略），这一结果不仅将问题归约为实数存在性理论（\exists\mathbb{R}），还支持构建值迭代算法。此外，我们证明阈值问题是NP难的。对于几乎确保可达性问题，我们证明了其NP完全性。我们引入个体随机化交替时态逻辑（IRATL）。该逻辑扩展了标准ATL框架以推理概率阈值，其语义专为缺乏共享随机源的联盟而设计。在实践层面，我们基于所提算法实现并评估了一个求解阈值与几乎确保问题的求解器。