Multi-agent safety verification using symmetry transformations

Hussein Sibai, Navid Mokhlesi, Chuchu Fan, Sayan Mitra

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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.

Original languageEnglish (US)
Title of host publicationTools and Algorithms for the Construction and Analysis of Systems- 26th International Conference, TACAS 2020, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Proceedings, Part I
EditorsArmin Biere, David Parker
PublisherSpringer
Pages173-190
Number of pages18
ISBN (Print)9783030451899
DOIs
StatePublished - Jan 1 2020
Event26th 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 - Dublin, Ireland
Duration: Apr 25 2020Apr 30 2020

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume12078 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference26th 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
CountryIreland
CityDublin
Period4/25/204/30/20

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Multi-agent safety verification using symmetry transformations'. Together they form a unique fingerprint.

  • Cite this

    Sibai, H., Mokhlesi, N., Fan, C., & Mitra, S. (2020). Multi-agent safety verification using symmetry transformations. In A. Biere, & D. Parker (Eds.), Tools and Algorithms for the Construction and Analysis of Systems- 26th International Conference, TACAS 2020, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Proceedings, Part I (pp. 173-190). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 12078 LNCS). Springer. https://doi.org/10.1007/978-3-030-45190-5_10