Using Symmetry Transformations in Equivariant Dynamical Systems for Their Safety Verification

Hussein Sibai, Navid Mokhlesi, Sayan Mitra

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

Abstract

In this paper, we investigate how symmetry transformations of equivariant dynamical systems can reduce the computation effort for safety verification. Symmetry transformations of equivariant systems map solutions to other solutions. We build upon this result, producing reachsets from other previously computed reachsets. We augment the standard simulation-based verification algorithm with a new procedure that attempts to verify the safety of the system starting from a new initial set of states by transforming previously computed reachsets. This new algorithm required the creation of a new cache-tree data structure for multi-resolution reachtubes. Our implementation has been tested on several benchmarks and has achieved significant improvements in verification time.

Original languageEnglish (US)
Title of host publicationAutomated Technology for Verification and Analysis- 17th International Symposium, AVTA 2019, Proceedings
EditorsYu-Fang Chen, Chih-Hong Cheng, Javier Esparza
PublisherSpringer
Pages98-114
Number of pages17
ISBN (Print)9783030317836
DOIs
StatePublished - 2019
Event17th International Symposium on Automated Technology for Verification and Analysis, ATVA 2019 - Taipei, Taiwan, Province of China
Duration: Oct 28 2019Oct 31 2019

Publication series

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

Conference

Conference17th International Symposium on Automated Technology for Verification and Analysis, ATVA 2019
Country/TerritoryTaiwan, Province of China
CityTaipei
Period10/28/1910/31/19

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint

Dive into the research topics of 'Using Symmetry Transformations in Equivariant Dynamical Systems for Their Safety Verification'. Together they form a unique fingerprint.

Cite this