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名玩家协同对抗对手以抵达一组目标状态。与传统设定不同，我们探究分布式随机化机制：团队玩家不共享随机源，其私有随机源对对手及彼此均不可见。我们证明无记忆策略足以解决阈值问题（即判定是否存在一种团队策略能确保获胜概率超过给定阈值），该结论不仅将该问题归入实数存在理论（∃ℝ）范畴，更启发了值迭代算法的构建。我们进一步证明阈值问题具有NP难度。对于几乎必然可达性问题，我们验证其NP完备性。本文提出个体随机化交替时序逻辑（IRATL），该逻辑在标准ATL框架基础上扩展了概率阈值推理能力，其语义专门为缺乏共享随机源的联盟设计。在实践层面，我们基于所开发算法实现并评估了针对阈值问题与几乎必然可达性问题的求解器。