A Set-based Approach to Model Checking of Nonlinear Systems
Politecnico di Milano, Italy
In this tutorial, we present an approach for verifying that a nonlinear dynamical system satisfies a given finite-horizon specification. The approach is based on reachability analysis via zonotopic set propagation and rests on the piecewise affine approximation of the nonlinear dynamics through a procedure that guarantees refinement inclusion. Possible extensions of the approach including safety and the enforcement of the specification when the system evolution can be affected by some control input are also discussed.
Short bio
Maria Prandini received her Ph.D. degree in Information Technology in 1998. From 1998 to 2000 she was a postdoctoral researcher at the Department of Electrical Engineering and Computer Sciences, University of California at Berkeley. She also held visiting positions at Delft University of Technology (1998), Cambridge University (2000), University of California at Berkeley (2005), and Swiss Federal Institute of Technology Zurich (2006). In 2002, she started as an assistant professor in systems and control at Politecnico di Milano, where she is currently a full professor.
Her research interests include stochastic hybrid systems, randomized algorithms, constrained control, system abstraction and verification, nonlinear identification, distributed optimization, and the application of control theory to air traffic management and energy systems.
She serves on the editorial board of Cyber Physical Systems, and previously of European Journal of Control, IEEE Transactions on Automatic Control, IEEE Transactions on Control Systems Technology and Nonlinear Analysis: Hybrid Systems.
From 2013 to 2015, she has been editor for Electronic Publications of the IEEE CSS. She was elected member of the IEEE CSS Board of Governors for a triennium (2015-17), and CSS Vice-President for Conference Activities in 2016 and 2017.