Multi-agent safety verification using symmetry transformations

TitleMulti-agent safety verification using symmetry transformations
Publication TypeConference Paper
Year of Publication2020
AuthorsSibai H, Mokhlesi N, Fan C, Mitra S
Conference Name26th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)
Date Publishedapr
ISBN Number9783030451899

We show that symmetry transformations and caching can enable scalable, and possibly unbounded, verification of multi-agent systems. Symmetry transformations map any solution of the system to another solution. 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 a virtual system which defines symmetry transformations for a broad class of agent models that visit waypoint sequences. Using this notion of a virtual system, we present a prototype tool CacheReach that builds a cache of reachsets, in a way that is agnostic of the representation of the reachsets and the reachability analysis method used. Our experimental evaluation of CacheReach shows up to 64{%} 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.