TY - GEN
T1 - Multi-agent safety verification using symmetry transformations
AU - Sibai, Hussein
AU - Mokhlesi, Navid
AU - Fan, Chuchu
AU - Mitra, Sayan
N1 - Publisher Copyright:
© 2020, The Author(s).
PY - 2020
Y1 - 2020
N2 - 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.
AB - 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.
UR - https://www.scopus.com/pages/publications/85083957213
U2 - 10.1007/978-3-030-45190-5_10
DO - 10.1007/978-3-030-45190-5_10
M3 - Conference contribution
AN - SCOPUS:85083957213
SN - 9783030451899
T3 - Lecture Notes in Computer Science
SP - 173
EP - 190
BT - Tools and Algorithms for the Construction and Analysis of Systems- 26th International Conference, TACAS 2020, held as part of the European Joint Conferenceson Theory and Practice of Software, ETAPS 2020, Proceedings
A2 - Biere, Armin
A2 - Parker, David
PB - Springer Science and Business Media Deutschland GmbH
T2 - 26th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2020, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020
Y2 - 25 April 2020 through 30 April 2020
ER -