|DESIMINI RICCARDO||Cycle: XXXIII |
Section: Systems and Control
Tutor: PIRODDI LUIGI
Advisor: PRANDINI MARIA Major Research topic
:Hybrid systems: computational approaches to verification and controlAbstract:
This thesis addresses automated verification and control design for hybrid systems, which are a class of dynamical systems characterized by interleaved continuous and discrete dynamics, typically modeling systems comprising physical and logical components and arising in various application domains. The idea is to adopt a unified modelling framework and develop a toolkit of computational methods based on reachability analysis for determining if a given hybrid system can satisfy some property related to its state evolution, in order to operate in a safe and/or efficient way. We consider the case when the system evolution is affected by some input variables which are disturbances and/or control inputs: if control inputs are available, then we are solving a control problem in the presence of uncertainty; if no control input is present, then, we are addressing a verification problem. We adopt as a modelling framework the class of discrete time PieceWise Affine (PWA) dynamical systems, which are hybrid systems characterized by a polyhedral partition of the continuous state/input space and a set of affine dynamics, each one associated with an element of the partition (called mode) representing the discrete state component. PWA systems are indeed equivalent to some classes of hybrid systems and can be adopted as an abstraction of the nonlinear smooth dynamics governing the continuous state evolution in a hybrid system. The developed toolkit of computational methods is inspired by existing approaches in the literature on, e.g., reachability analysis, reach set representation and reduction, invariant set computation, and further extend and combine them within a comprehensive framework, thus enhancing the applicability of model-based techniques for PWA systems verification and control. Interestingly, also the parameter varying case is considered.