@inproceedings{22617,
  abstract     = {Consider a 4-player version of Matching Pennies where a team of three players competes against the Devil. Each player simultaneously says "Heads" or "Tails". The team wins if all four choices match; otherwise the Devil wins. If all team players randomise independently, they win with probability 1/8; if all players share a common source of randomness, they win with probability 1/2. What happens when each pair of team players shares a source of randomness? Can the team do better than win with probability 1/4? The surprising (and nontrivial) answer is yes!
We introduce Dicey Games, a formal framework motivated by the study of distributed systems with shared sources of randomness (of which the above example is a specific instance). We characterise the existence, representation and computational complexity of optimal strategies in Dicey Games, and we study the problem of allocating limited sources of randomness optimally within a team.},
  author       = {Brice, Leonard J and Henzinger, Thomas A and Thejaswini, K. S.},
  booktitle    = {41st Annual Symposium on Logic in Computer Science},
  isbn         = {9783959774345},
  issn         = {1868-8969},
  keywords     = {Concurrent games, Shared randomness, Topology, Algebraic Geometry},
  location     = {Lisbon, Portugal},
  publisher    = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik},
  title        = {{Dicey games: Shared sources of randomness in distributed systems}},
  doi          = {10.4230/LIPIcs.LICS.2026.23},
  volume       = {380},
  year         = {2026},
}

@inproceedings{22717,
  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 (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.},
  author       = {Brice, Leonard J and Henzinger, Thomas A and Montaseri, Alipasha and Shafiee, Ali and Thejaswini, K. S.},
  booktitle    = {38th International Conference on Computer Aided Verification},
  isbn         = {9783032325181},
  issn         = {1611-3349},
  location     = {Lisbon, Portugal},
  pages        = {215--236},
  publisher    = {Springer Nature},
  title        = {{Randomise alone, reach as a team}},
  doi          = {10.1007/978-3-032-32519-8_12},
  volume       = {16682},
  year         = {2026},
}