Report Title: Reachability Analysis of Learning enabled Cyber Physical Systems

Report time: 09:00, December 29th Offline report location: B1002, Science Building

Tencent Meeting Number: 763-614-103

Host: Professor Zhang Min

Abstract:

Neural networks have been increasingly used as the central decision makers in a variety of tasks. However, the use of neural-network controllers also gives rise to new challenges on verifying the correctness of the resulting closed-loop control systems especially in safety-critical settings. This talk focuses on computing the reachable sets of Cyber-Physical Systems (CPS) which are defined by neural network-controlled nonlinear continuous dynamics. Reachability analysis is the core of most formal verification tasks, and is notoriously difficult even on linear dynamics with simple switching logic. In the talk,  we will present the main framework of using flowpipe construction for learning-enabled CPS. Three techniques will be introduced for computing higher-order overapproximations for reachable sets. We will show how the dependencies among the state variables during the system evolution can be accurately approximated by our methods. Experimental evaluations will also be given to demonstrate the effectiveness of the methods.

Introduction of Lectuer:

Dr. Xin Chen is currently an assistant professor at the University of Dayton in Dayton, Ohio. He received his Ph.D. in Computer Science from RWTH Aachen University in 2015, and was a postdoctoral research associate at the University of Colorado, Boulder. Dr. Chen's main research interests lie in the area of solving verification and synthesis problems for autonomous systems using formal methods. He is also the sole-PI of an on-going research project funded by the U.S. Air Force Research Laboratory.