Randomise alone, reach as a team

conference paper Randomise alone, reach as a team published yes Leonard J Brice author ce3b3409-db6c-11f0-aa64-ad678f7fd937 Thomas A Henzinger author 40876CD8-F248-11E8-B48F-1D18A9856A870000-0002-2985-7724 Alipasha Montaseri author 709a7f96-8896-11f0-9809-d75612fc0f2e Ali Shafiee author 2783031a-7378-11f0-b2d0-f17f1db2ebad K. S. Thejaswini author ToHe department GradSch department CAV: Computer Aided Verification Vigilant Algorithmic Monitoring of Software project 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 (ER) 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. https://research-explorer.ista.ac.at/download/22717/22724/2026_LNCS_Brice.pdf application/pdfno https://creativecommons.org/licenses/by/4.0/ Springer Nature2026Lisbon, Portugal eng 38th International Conference on Computer Aided Verification 0302-9743 1611-3349 9783032325181 2603.0709410.1007/978-3-032-32519-8_12 16682215-236 L. J. Brice, T. A. Henzinger, A. Montaseri, A. Shafiee, and K. S. Thejaswini, “Randomise alone, reach as a team,” in 38th International Conference on Computer Aided Verification, Lisbon, Portugal, 2026, vol. 16682, pp. 215–236. Brice LJ, Henzinger TA, Montaseri A, Shafiee A, Thejaswini KS. 2026. Randomise alone, reach as a team. 38th International Conference on Computer Aided Verification. CAV: Computer Aided Verification vol. 16682, 215–236. Brice, L. J., Henzinger, T. A., Montaseri, A., Shafiee, A., & Thejaswini, K. S. (2026). Randomise alone, reach as a team. In 38th International Conference on Computer Aided Verification (Vol. 16682, pp. 215–236). Lisbon, Portugal: Springer Nature. <a href="https://doi.org/10.1007/978-3-032-32519-8_12">https://doi.org/10.1007/978-3-032-32519-8_12</a> Brice LJ, Henzinger TA, Montaseri A, Shafiee A, Thejaswini KS. Randomise alone, reach as a team. In: 38th International Conference on Computer Aided Verification. Vol 16682. Springer Nature; 2026:215-236. doi:<a href="https://doi.org/10.1007/978-3-032-32519-8_12">10.1007/978-3-032-32519-8_12</a> L.J. Brice, T.A. Henzinger, A. Montaseri, A. Shafiee, K.S. Thejaswini, in:, 38th International Conference on Computer Aided Verification, Springer Nature, 2026, pp. 215–236. Brice, Leonard J., et al. “Randomise Alone, Reach as a Team.” 38th International Conference on Computer Aided Verification, vol. 16682, Springer Nature, 2026, pp. 215–36, doi:<a href="https://doi.org/10.1007/978-3-032-32519-8_12">10.1007/978-3-032-32519-8_12</a>. Brice, Leonard J, Thomas A Henzinger, Alipasha Montaseri, Ali Shafiee, and K. S. Thejaswini. “Randomise Alone, Reach as a Team.” In 38th International Conference on Computer Aided Verification, 16682:215–36. Springer Nature, 2026. <a href="https://doi.org/10.1007/978-3-032-32519-8_12">https://doi.org/10.1007/978-3-032-32519-8_12</a>. 227172026-08-16T22:01:44Z2026-08-18T06:55:38Z