# Multi-Agent Verification and Control with Probabilistic Model Checking

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

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Builds on 10 of its 26 references that are in the map.
- First posted on arXiv 5 Aug 2023.

## Builds on (most cited first, 10 of 10)

- [Multi-Agent Reinforcement Learning with Temporal Logic Specifications](https://mlsanity.com/paper/2102.00582/) (2021)
- [TEMPEST -- Synthesis Tool for Reactive Systems and Shields in Probabilistic Environments](https://mlsanity.com/paper/2105.12588/) (2021)
- [Value Iteration for Simple Stochastic Games: Stopping Criterion and Learning Algorithm](https://mlsanity.com/paper/1804.04901/) (2018)
- [Automatic Verification of Concurrent Stochastic Systems](https://mlsanity.com/paper/2008.04613/) (2020)
- [Comparison of Algorithms for Simple Stochastic Games (Full Version)](https://mlsanity.com/paper/2008.09465/) (2020)
- [Strategy Synthesis for Zero-Sum Neuro-Symbolic Concurrent Stochastic Games](https://mlsanity.com/paper/2202.06255/) (2022)
- [Correlated Equilibria and Fairness in Concurrent Stochastic Games](https://mlsanity.com/paper/2201.09702/) (2022)
- [Finite-horizon Equilibria for Neuro-symbolic Concurrent Stochastic Games](https://mlsanity.com/paper/2205.07546/) (2022)
- [Symbolic Verification and Strategy Synthesis for Turn-based Stochastic Games](https://mlsanity.com/paper/2211.06141/) (2022)
- [Stochastic Games with Lexicographic Reachability-Safety Objectives](https://mlsanity.com/paper/2005.04018/) (2020)

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

- [From Glue-Code to Protocols: A Critical Analysis of A2A and MCP Integration for Scalable Agent Systems](https://mlsanity.com/paper/2505.03864/) (2025)

## Abstract (arXiv)

Probabilistic model checking is a technique for formal automated reasoning about software or hardware systems that operate in the context of uncertainty or stochasticity. It builds upon ideas and techniques from a diverse range of fields, from logic, automata and graph theory, to optimisation, numerical methods and control. In recent years, probabilistic model checking has also been extended to integrate ideas from game theory, notably using models such as stochastic games and solution concepts such as equilibria, to formally verify the interaction of multiple rational agents with distinct objectives. This provides a means to reason flexibly about agents acting in either an adversarial or a collaborative fashion, and opens up opportunities to tackle new problems within, for example, artificial intelligence, robotics and autonomous systems. In this paper, we summarise some of the advances in this area, and highlight applications for which they have already been used. We discuss how the strengths of probabilistic model checking apply, or have the potential to apply, to the multi-agent setting and outline some of the key challenges required to make further progress in this field.