TY - GEN
T1 - Using Symmetry Transformations in Equivariant Dynamical Systems for Their Safety Verification
AU - Sibai, Hussein
AU - Mokhlesi, Navid
AU - Mitra, Sayan
N1 - Funding Information:
Acknowledgments. 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.
Publisher Copyright:
© 2019, Springer Nature Switzerland AG.
PY - 2019
Y1 - 2019
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=85076093691&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85076093691&partnerID=8YFLogxK
U2 - 10.1007/978-3-030-31784-3_6
DO - 10.1007/978-3-030-31784-3_6
M3 - Conference contribution
AN - SCOPUS:85076093691
SN - 9783030317836
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 98
EP - 114
BT - Automated Technology for Verification and Analysis- 17th International Symposium, AVTA 2019, Proceedings
A2 - Chen, Yu-Fang
A2 - Cheng, Chih-Hong
A2 - Esparza, Javier
PB - Springer
T2 - 17th International Symposium on Automated Technology for Verification and Analysis, ATVA 2019
Y2 - 28 October 2019 through 31 October 2019
ER -