# An Abstraction-based Method to Check Multi-Agent Deep Reinforcement-Learning Behaviors

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

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Builds on 6 of its 33 references that are in the map.
- First posted on arXiv 2 Feb 2021.

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

- [Dueling Network Architectures for Deep Reinforcement Learning](https://mlsanity.com/paper/1511.06581/) (2015)
- [Safe Reinforcement Learning via Shielding](https://mlsanity.com/paper/1708.08611/) (2017)
- [End-to-End Safe Reinforcement Learning through Barrier Functions for Safety-Critical Continuous Control Tasks](https://mlsanity.com/paper/1903.08792/) (2019)
- [An Introduction to Deep Reinforcement Learning](https://mlsanity.com/paper/1811.12560/) (2018)
- [Multiagent Cooperation and Competition with Deep Reinforcement Learning](https://mlsanity.com/paper/1511.08779/) (2015)
- [A storm is Coming: A Modern Probabilistic Model Checker](https://mlsanity.com/paper/1702.04311/) (2017)

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

- [Synthesising Robust Controllers for Robot Collectives with Recurrent Tasks: A Case Study](https://mlsanity.com/paper/2411.14371/) (2024)

## Abstract (arXiv)

Multi-agent reinforcement learning (RL) often struggles to ensure the safe behaviours of the learning agents, and therefore it is generally not adapted to safety-critical applications. To address this issue, we present a methodology that combines formal verification with (deep) RL algorithms to guarantee the satisfaction of formally-specified safety constraints both in training and testing. The approach we propose expresses the constraints to verify in Probabilistic Computation Tree Logic (PCTL) and builds an abstract representation of the system to reduce the complexity of the verification step. This abstract model allows for model checking techniques to identify a set of abstract policies that meet the safety constraints expressed in PCTL. Then, the agents' behaviours are restricted according to these safe abstract policies. We provide formal guarantees that by using this method, the actions of the agents always meet the safety constraints, and provide a procedure to generate an abstract model automatically. We empirically evaluate and show the effectiveness of our method in a multi-agent environment.