Data-Driven Safety Verification using Reachability Analysis
Authors
Amr Alanwar, KTH
Date and Time
Oct 13th 2021, 15:15 - 16:00
Location
Zoom: https://uu-se.zoom.us/j/61183647419
Abstract
Reachability analysis computes the set of reachable states of a system with uncertain initial states, inputs, and parameters. One major application of reachability analysis is the formal verification of embedded systems. However, obtaining an accurate model for such systems to compute model-based reachable sets is a challenging task. It is now possible to obtain input/output data from such systems, making it feasible to develop data-driven reachability analysis. In this seminar, I will present our algorithms for computing data-driven reachable sets with formal guarantees. Our algorithms support incorporating side information in terms of signal temporal logic to decrease the conservatism of the reachable sets. Then, through their application in providing a guaranteed safe reinforcement learning for black-box systems, I will show the effectiveness of our algorithms.
Author Bio
Amr Alanwar is a postdoctoral researcher at KTH Royal Institute of Technology and offered an assistant professor position at Jacobs University. He got his Ph.D. with the Cyber-Physical Systems Group at the Technical University of Munich (TUM). Before that, he was a research assistant at the Networked & Embedded Systems Laboratory at the University of California, Los Angeles (UCLA). He also has industrial experience as a research and development engineer in Mentor Graphics and Morpho companies. Amr won the Best Demonstration Paper Award at the 16th ACM/IEEE International Conference on Information Processing in Sensor Networks (IPSN/CPS week) and was a finalist in the Qualcomm Innovation Fellowship for two years in a row. He received his B.Sc. and M.Sc from Ain Shams University. His current research interests include safety, privacy, and general topics in embedded systems.