# Turn-based Multi-Agent Reinforcement Learning Model Checking

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

## Key facts

- Cited by 3 papers in the map (data through 14 Oct 2026).
- Builds on 17 of its 45 references that are in the map.
- First posted on arXiv 6 Jan 2025.

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

- [Playing Atari with Deep Reinforcement Learning](https://mlsanity.com/paper/1312.5602/) (2013)
- [Dota 2 with Large Scale Deep Reinforcement Learning](https://mlsanity.com/paper/1912.06680/) (2019)
- [Omega-Regular Objectives in Model-Free Reinforcement Learning](https://mlsanity.com/paper/1810.00950/) (2018)
- [Environment-Independent Task Specifications via GLTL](https://mlsanity.com/paper/1704.04341/) (2017)
- [The Probabilistic Model Checker Storm](https://mlsanity.com/paper/2002.07080/) (2020)
- [Scalar reward is not enough: A response to Silver, Singh, Precup and Sutton (2021)](https://mlsanity.com/paper/2112.15422/) (2021)
- [Deep Multiagent Reinforcement Learning: Challenges and Directions](https://mlsanity.com/paper/2106.15691/) (2021)
- [Reinforcement Learning with Probabilistic Guarantees for Autonomous Driving](https://mlsanity.com/paper/1904.07189/) (2019)
- [COOL-MC: A Comprehensive Tool for Reinforcement Learning and Model Checking](https://mlsanity.com/paper/2209.07133/) (2022)
- [Verifiably Safe Off-Model Reinforcement Learning](https://mlsanity.com/paper/1902.05632/) (2019)
- [Statistically Model Checking PCTL Specifications on Markov Decision Processes via Reinforcement Learning](https://mlsanity.com/paper/2004.00273/) (2020)
- [Specification-Guided Learning of Nash Equilibria with High Social Welfare](https://mlsanity.com/paper/2206.03348/) (2022)
- [Optimizing Expectation with Guarantees in POMDPs (Technical Report)](https://mlsanity.com/paper/1611.08696/) (2016)
- [Feature-Based Interpretable Reinforcement Learning based on State-Transition Models](https://mlsanity.com/paper/2105.07099/) (2021)
- [Learning Safe Unlabeled Multi-Robot Planning with Motion Constraints](https://mlsanity.com/paper/1907.05300/) (2019)
- [Symbolic Verification and Strategy Synthesis for Turn-based Stochastic Games](https://mlsanity.com/paper/2211.06141/) (2022)
- [Verification and Control of Turn-Based Probabilistic Real-Time Games](https://mlsanity.com/paper/1906.09142/) (2019)

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

- [COOL-MC: Verifying and Explaining RL Policies for Platelet Inventory Management](https://mlsanity.com/paper/2603.02396/) (2026)
- [COOL-MC: Verifying and Explaining RL Policies for Multi-bridge Network Maintenance](https://mlsanity.com/paper/2603.07546/) (2026)
- [Automated Testing of LLM-Based Post Hoc Explainers Using Model Checking as an Oracle](https://mlsanity.com/paper/2608.30581/) (2026)

## Abstract (arXiv)

In this paper, we propose a novel approach for verifying the compliance of turn-based multi-agent reinforcement learning (TMARL) agents with complex requirements in stochastic multiplayer games. Our method overcomes the limitations of existing verification approaches, which are inadequate for dealing with TMARL agents and not scalable to large games with multiple agents. Our approach relies on tight integration of TMARL and a verification technique referred to as model checking. We demonstrate the effectiveness and scalability of our technique through experiments in different types of environments. Our experiments show that our method is suited to verify TMARL agents and scales better than naive monolithic model checking.