# Collision Avoidance Verification of Multiagent Systems with Learned Policies

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

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 9 of its 19 references that are in the map.
- First posted on arXiv 5 Mar 2024.

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

- [Learning Decentralized Controllers for Robot Swarms with Graph Neural Networks](https://mlsanity.com/paper/1903.10527/) (2019)
- [Multi-Agent Connected Autonomous Driving using Deep Reinforcement Learning](https://mlsanity.com/paper/1911.04175/) (2019)
- [Reach-SDP: Reachability Analysis of Closed-Loop Systems with Neural Network Controllers via Semidefinite Programming](https://mlsanity.com/paper/2004.07876/) (2020)
- [Reachability Analysis of Neural Feedback Loops](https://mlsanity.com/paper/2108.04140/) (2021)
- [Backward Reachability Analysis of Neural Feedback Loops: Techniques for Linear and Nonlinear Systems](https://mlsanity.com/paper/2209.14076/) (2022)
- [Backward Reachability Analysis for Neural Feedback Loops](https://mlsanity.com/paper/2204.08319/) (2022)
- [Strategy Synthesis for Zero-Sum Neuro-Symbolic Concurrent Stochastic Games](https://mlsanity.com/paper/2202.06255/) (2022)
- [Scalable Forward Reachability Analysis of Multi-Agent Systems with Neural Network Controllers](https://mlsanity.com/paper/2309.03846/) (2023)
- [Partially Observable Stochastic Games with Neural Perception Mechanisms](https://mlsanity.com/paper/2310.11566/) (2023)

## Abstract (arXiv)

For many multiagent control problems, neural networks (NNs) have enabled promising new capabilities. However, many of these systems lack formal guarantees (e.g., collision avoidance, robustness), which prevents leveraging these advances in safety-critical settings. While there is recent work on formal verification of NN-controlled systems, most existing techniques cannot handle scenarios with more than one agent. To address this research gap, this paper presents a backward reachability-based approach for verifying the collision avoidance properties of Multi-Agent Neural Feedback Loops (MA-NFLs). Given the dynamics models and trained control policies of each agent, the proposed algorithm computes relative backprojection sets by (simultaneously) solving a series of Mixed Integer Linear Programs (MILPs) offline for each pair of agents. We account for state measurement uncertainties, making it well aligned with real-world scenarios. Using those results, the agents can quickly check for collision avoidance online by solving low-dimensional Linear Programs (LPs). We demonstrate the proposed algorithm can verify collision-free properties of a MA-NFL with agents trained to imitate a collision avoidance algorithm (Reciprocal Velocity Obstacles). We further demonstrate the computational scalability of the approach on systems with up to 10 agents.