# Automatic Verification of Concurrent Stochastic Systems

arXiv: https://arxiv.org/abs/2008.04613 · HTML: https://mlsanity.com/paper/2008.04613/

## Key facts

- Cited by 7 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 11 Aug 2020.

## Built on by (most cited first, 7 of 7)

- [Strategy Synthesis for Zero-Sum Neuro-Symbolic Concurrent Stochastic Games](https://mlsanity.com/paper/2202.06255/) (2022)
- [Counterfactual Reasoning for Causal Responsibility Attribution in Probabilistic Multi-Agent Systems](https://mlsanity.com/paper/2605.13077/) (2026)
- [Multi-Agent Verification and Control with Probabilistic Model Checking](https://mlsanity.com/paper/2308.02829/) (2023)
- [Responsibility-aware Strategic Reasoning in Probabilistic Multi-Agent Systems](https://mlsanity.com/paper/2411.00146/) (2024)
- [Robust Verification of Concurrent Stochastic Games](https://mlsanity.com/paper/2601.12003/) (2026)
- [Expectation vs. Reality: Towards Verification of Psychological Games](https://mlsanity.com/paper/2411.05599/) (2024)
- [Robust PAC Learning of Concurrent Stochastic Games](https://mlsanity.com/paper/2609.04189/) (2026)

## Abstract (arXiv)

Automated verification techniques for stochastic games allow formal reasoning about systems that feature competitive or collaborative behaviour among rational agents in uncertain or probabilistic settings. Existing tools and techniques focus on turn-based games, where each state of the game is controlled by a single player, and on zero-sum properties, where two players or coalitions have directly opposing objectives. In this paper, we present automated verification techniques for concurrent stochastic games (CSGs), which provide a more natural model of concurrent decision making and interaction. We also consider (social welfare) Nash equilibria, to formally identify scenarios where two players or coalitions with distinct goals can collaborate to optimise their joint performance. We propose an extension of the temporal logic rPATL for specifying quantitative properties in this setting and present corresponding algorithms for verification and strategy synthesis for a variant of stopping games. For finite-horizon properties the computation is exact, while for infinite-horizon it is approximate using value iteration. For zero-sum properties it requires solving matrix games via linear programming, and for equilibria-based properties we find social welfare or social cost Nash equilibria of bimatrix games via the method of labelled polytopes through an SMT encoding. We implement this approach in PRISM-games, which required extending the tool's modelling language for CSGs, and apply it to case studies from domains including robotics, computer security and computer networks, explicitly demonstrating the benefits of both CSGs and equilibria-based properties.