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 & tables
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)
Appendix figures & tables7 assets
Supplementary material from the paper’s appendix.
Appendix
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 1 .
Figure 6: Visualizations of the seven scenarios used for the almost-sure experiment. All scenarios involve two team players. Green nodes indicate the team’s starting positions, while the red node indicates the opponent’s. The results are available in Table 4 .
Figure 7: The four benchmark scenarios for the robot game. Robots are shown as circles ( Ri ), and the target is marked with T.
Scenario
Team
States
Algorithm
Individual Randomness
Shared Randomness
Trans
Time
Val
Iter
Time
Val
Iter
1
2
27 512
ETR-Direct
T.O.
N/F
N/A
T.O.
N/F
N/A
VI-ETR
4.42
0.290
6
0.40
0.500
2
VI-OPT
0.54
0.290
6
0.02
0.500
2
VI-Hybrid
0.58
0.290
6
0.05
0.500
2
PRISM
-
-
N/A
1.58
0.500
N/A
Appendix
Table 1: Experimental results for the six scenarios illustrated in Figure 5 . For each algorithm, the table lists the execution time in seconds, the computed value, and the number of iterations required for convergence. The label “T.O.” denotes a timeout after 600 seconds. In cases where an algorithm timed out, we report the value obtained from the final completed iteration. “N/F” indicates Not Found.
Scenario
Team Size
States
Algorithm
Individual Randomness
Shared Randomness
Trans
Time
Value
Iters
Time
Value
Iters
1
2
16 2000
ETR-Direct
T.O.
N/F
N/A
T.O.
N/F
N/A
VI-ETR
7.86
0.293
6
4.86
0.324
6
VI-OPT
0.56
0.274
6
0.72
0.323
6
VI-Hybrid
5.35
0.293
6
2.27
0.324
6
PRISM
-
-
N/A
1.47
0.324
N/A
Appendix
Table 2: Experimental results for the four scenarios illustrated in Figure 7 . For each algorithm, the table lists the execution time in seconds, the computed value, and the number of iterations required for convergence. The label "T.O." denotes a timeout after 600 seconds. In cases where an algorithm timed out, we report the value obtained from the final completed iteration.
Parameters
States
Algorithm
Individual Randomness
Shared Randomness
Trans
Time
Value
Iters
Time
Value
Iters
C=2, B=[1, 1]
5 135
ETR-Direct
T.O.
N/F
N/A
T.O.
N/F
N/A
VI-ETR
0.33
0.250
3
0.25
0.250
3
VI-OPT
0.62
0.246
46
0.02
0.250
3
VI-Hybrid
0.08
0.250
3
0.03
0.250
3
PRISM
-
-
N/A
1.38
0.250
N/A
Appendix
Table 3: Performance comparison of algorithms on the jamming multi-channel radio system benchmark. Each scenario is defined by the number of channels C followed by the initial buffer sizes [B1,…,Bk] for k players. We report the number of states, number of transitions, execution time in seconds, computed game value V , and the number of iterations for the value iteration algorithms. “T.O.” indicates the algorithm exceeded the 600s time limit. For instances that timed out, we provide the value from the last completed iteration, where available.
Scenario
States Trans
Method
Individual Randomness
Shared Randomness
Time
Result
Time
Result
1
27 729
SAT-Direct
0.02
UNSAT
0.02
UNSAT
PRISM-Qual
–
–
1.62
UNSAT
2
64 1728
SAT-Direct
0.09
SAT
0.09
SAT
PRISM-Qual
–
–
1.42
SAT
3
125 4913
SAT-Direct
0.29
UNSAT
0.33
UNSAT
Appendix
Table 4: Experimental results for the almost-sure reachability problem on the Pursuit-Evasion benchmark. The scenarios are illustrated in Figure 6 . For each scenario, the table lists the execution time in seconds and the outcome. We compare our SAT-Direct algorithm (under both individual and shared randomness) against the PRISM-games baseline (which supports only shared randomness). A result of SAT indicates that the target is almost-surely reachable, while UNSAT indicates that it is not.
Institute of Science and Technology Austria Klosterneuburg, Austria · École Polytechnique Fédérale de Lausanne Lausanne, Switzerland · Université libre de Bruxelles Brussels, Belgium