Reachability Analysis of Linear, Nonlinear, and Hybrid Systems

Matthias Althoff, Department of Electrical and Computer Engineering,  Carnegie Mellon University

The necessity of automatic tools for the verification of dynamic systems is constantly increasing due to the growing complexity of the technical world. A possible answer to this problem is the verification of hybrid systems based on reachability analysis. One of the biggest challenges in reachability analysis is the curse of dimension. As a possible solution to this problem, zonotopes have been suggested as a representation of reachable sets by e.g. W. Kühn and A. Girard. The performance of zonotopes for linear systems is exceptional; however there are still obstacles to overcome when zonotopes are used for nonlinear and hybrid systems which are addressed in this talk.                                 
                                                                                                
First, an approach for linear systems with uncertain parameters is introduced. This approach is then extended to nonlinear system based on conservative linearization, i.e. the linearization error is added as an uncertain input. Next, the extension to hybrid systems is presented. The talk closes with two application examples: safety verification of autonomous cars and invariant verification of phase-locked loops.
                                                                                                

BIO:                                                                                          
                                                                                                
Matthias Althoff is a postdoctoral researcher in the group of Prof. Bruce Krogh, Departmentof Electrical and Computer Engineering at Carnegie Mellon University. He received his Ph.D. degree at the Technische Universität München, Germany, and the diploma engineering degree in Mechanical Engineering in 2005 from the same university. His research interests include (stochastic) reachability analysis of continuous and hybrid systems and their application to engineering problems, such as the safety analysis of autonomous cars, intelligent road intersections, and digital-analog circuits.