Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Collision Avoidance Verification of Multiagent Systems with Learned Policies

Zihao Dong, Shayegan Omidshafiei, Michael Everett

TL;DR

This work tackles the lack of formal collision guarantees for multiagent systems with neural controllers by introducing ReBAR and ReBAR-MA, a relative backward reachability framework. Offline, it computes conservative RBPOA approximations via MILPs in a relative coordinate frame; online, it provides fast safety checks with LPs under state uncertainty. The methods are demonstrated on MA-NFLs trained to emulate RVO and scale to systems with up to 10 agents, with clear trade-offs between offline verification time and online safety assurance. Pairwise verification enables scalable multiagent safety guarantees, contributing a practical approach for real-time collision avoidance in safety-critical applications. Future directions include handling more general activation functions and decentralized observation spaces.

Abstract

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.

Collision Avoidance Verification of Multiagent Systems with Learned Policies

TL;DR

This work tackles the lack of formal collision guarantees for multiagent systems with neural controllers by introducing ReBAR and ReBAR-MA, a relative backward reachability framework. Offline, it computes conservative RBPOA approximations via MILPs in a relative coordinate frame; online, it provides fast safety checks with LPs under state uncertainty. The methods are demonstrated on MA-NFLs trained to emulate RVO and scale to systems with up to 10 agents, with clear trade-offs between offline verification time and online safety assurance. Pairwise verification enables scalable multiagent safety guarantees, contributing a practical approach for real-time collision avoidance in safety-critical applications. Future directions include handling more general activation functions and decentralized observation spaces.

Abstract

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.
Paper Structure (14 sections, 4 theorems, 15 equations, 3 figures, 4 algorithms)

This paper contains 14 sections, 4 theorems, 15 equations, 3 figures, 4 algorithms.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Multiagent System Dynamics
  4. Neural Network Controller Architecture
  5. Collision Sets
  6. Backreachable & Backprojection Set
  7. Approach
  8. Relative Backreachable & Backprojection Sets
  9. Two Agent Verification
  10. Scaling to More Agents
  11. Experiment
  12. Two Agent Verification
  13. Runtime and Scalability
  14. Conclusion

Key Result

Lemma III.1

A system with 2 agents $i,j$ with closed-loop dynamics function $f^{(i,j)}$ and collision set $\mathcal{C}^{(i,j)}$ is verified safe if $\bar{\mathcal{P}}_{-1}(\mathcal{C}^{(i,j)}) \subseteq \mathcal{C}^{(i,j)}$.

Figures (3)

  • Figure 1: Complex interactions between agents present challenges in formal safety verification. This analysis is further complicated when the agents are using NN control policies.
  • Figure 2: (a): Forward reachable sets of agent 1 (blue) intersect with agent 2 (red). Unable to verify system safety despite no simulated rollouts (green lines) enters agent 2. (b): Result of ReBAR (magenta) is within agent 2, system is verified safe.
  • Figure 3: $\mathcal{C}^{(i,j)}$ (red) is a convex polytope around agent $i$; $\bar{\mathcal{P}}_{-1}(\mathcal{C}^{(i,j)})$ (light grey) is the tightest convex polytope of $\mathcal{P}_{-1}(\mathcal{C}^{(i,j)})$ (grey) using the given facets; $\mathcal{R}_{-1}(\mathcal{C}^{(i,j)})$ (green) contains all states that $\exists u \in \mathcal{U}$ s.t. agent $i,j$ collides

Theorems & Definitions (12)

  • Definition III.1: Verified Safe
  • Lemma III.1
  • proof
  • Definition III.2: Multi-Agent Verified Safe
  • Lemma III.2
  • proof
  • Definition IV.1: Verified Safe
  • Lemma IV.1
  • proof
  • Definition IV.2: Multi-Agent Verified Safe
  • ...and 2 more