Multi-Agent Safety Verification using Symmetry
Transformations
Hussein Sibai , Navid Mokhlesi , Chuchu Fan , and Sayan Mitra
{sibai2,navidm2,cfan10,mitras}@illinois.edu
University of Illinois, Urbana IL 61801, USA
Abstract. 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.
1 Introduction
As the cornerstone for safety verification of dynamical and hybrid systems, reachability
analysis has attracted attention and has delivered automatic analysis of automotive,
aerospace, and medical applications [2,24,17,11]. Notable advances from the last few
years include the development of the generalized star data-structure [14] and the HyLaa
tool [3] which can analyze massive linear models [4]; Taylor model based reachability
analysis algorithms for nonlinear systems and their implementations in Flow* [7]; and a
simulation-based algorithm that guarantees locally optimal precision [15].
Exact symbolic reachability analysis of nonlinear models is generally hard. One
prominent approach is based on generalizing individual behaviors or simulations to
cover a whole set of behaviors. The idea was pioneered in [10] and implemented in
Breach [9] with sound generalization guarantees for linear models based on sensitivity
analysis. Subsequently, the idea has been significantly extended to cover nonlinear,
hybrid, and black-box models and it has been implemented in tools like C2E2 and
DryVR [12,19,17,16].
In all of the above, a single behavior ξ of the system from an initial state, is generalized to a compact set of neighboring behaviors that contains all the behaviors starting
The authors are supported by a research grant from The Boeing Company and a research grant
from NSF (CPS 1739966). We would like to thank John L. Olson and Arthur S. Younger from
The Boeing Company for valuable technical discussions.
© The Author(s) 2020
A. Biere and D. Parker (Eds.): TACAS 2020, LNCS 12078, pp. 173–190, 2020.
https://doi.org/10.1007/978-3-030-45190-5_10
TACAS
Evaluation
Artifact
2020
Accepted
Transformations
Hussein Sibai , Navid Mokhlesi , Chuchu Fan , and Sayan Mitra
{sibai2,navidm2,cfan10,mitras}@illinois.edu
University of Illinois, Urbana IL 61801, USA
Abstract. 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.
1 Introduction
As the cornerstone for safety verification of dynamical and hybrid systems, reachability
analysis has attracted attention and has delivered automatic analysis of automotive,
aerospace, and medical applications [2,24,17,11]. Notable advances from the last few
years include the development of the generalized star data-structure [14] and the HyLaa
tool [3] which can analyze massive linear models [4]; Taylor model based reachability
analysis algorithms for nonlinear systems and their implementations in Flow* [7]; and a
simulation-based algorithm that guarantees locally optimal precision [15].
Exact symbolic reachability analysis of nonlinear models is generally hard. One
prominent approach is based on generalizing individual behaviors or simulations to
cover a whole set of behaviors. The idea was pioneered in [10] and implemented in
Breach [9] with sound generalization guarantees for linear models based on sensitivity
analysis. Subsequently, the idea has been significantly extended to cover nonlinear,
hybrid, and black-box models and it has been implemented in tools like C2E2 and
DryVR [12,19,17,16].
In all of the above, a single behavior ξ of the system from an initial state, is generalized to a compact set of neighboring behaviors that contains all the behaviors starting
The authors are supported by a research grant from The Boeing Company and a research grant
from NSF (CPS 1739966). We would like to thank John L. Olson and Arthur S. Younger from
The Boeing Company for valuable technical discussions.
© The Author(s) 2020
A. Biere and D. Parker (Eds.): TACAS 2020, LNCS 12078, pp. 173–190, 2020.
https://doi.org/10.1007/978-3-030-45190-5_10
TACAS
Evaluation
Artifact
2020
Accepted