Multi-Agent Safety Verification using Symmetry Transformations

TL;DR

This paper introduces a symmetry-based caching method for scalable safety verification of multi-agent systems, demonstrating significant computational savings through a prototype tool called CacheReach.

Contribution

It develops a virtual system framework for symmetry transformations and presents CacheReach, a tool that leverages these transformations for efficient reachability analysis.

Findings

Up to 66% reduction in verification time.

Effective for both linear and nonlinear multi-agent models.

Demonstrates scalability with complex agent sequences.

Abstract

We show that symmetry transformations and caching can enable scalable, and possibly unbounded, verification of multi-agent systems. Symmetry transformations map solutions and to other solutions. We show that this property can be used to transform cached reachsets to compute new reachsets, for hybrid and multi-agent models. We develop a notion of virtual system which define symmetry transformations for a broad class of agent models that visit waypoint sequences. Using this notion of virtual system, we present a prototype tool CacheReach that builds a cache of reachtubes for this system, in a way that is agnostic of the representation of the reachsets and the reachability analysis subroutine used. Our experimental evaluation of CacheReach shows up to 66% savings in safety verification computation time on multi-agent systems with 3-dimensional linear and 4-dimensional nonlinear fixed-wing aircraft models following sequences of waypoints. These savings and our theoretical results illustrate the potential benefits of using symmetry-based caching in the safety verification of multi-agent systems.