Hybrid systems : computational approaches to verification and control

This thesis addresses formal 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 set-based computational methods based on reachability and invariant analysis for determining if a given hybrid system can satisfy some property related to its state evolution and operate in a safe and/or efficient way. We consider the case when the system evolution is affected by input variables which can either be disturbances or control inputs: if control inputs are available, then, we are solving a control problem trying to enforce a certain behavior, despite the presence of uncertainty; if no control input is present, then, we are addressing a verification problem. We adopt as 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 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 reachability analysis, reach set representation and reduction, invariant set computation, and further extend and combine them within a comprehensive framework, including also the parameter varying case, thus enhancing the applicability of model-based techniques for PWA systems verification and control.

In questa tesi vengono affrontati problemi di verifica e controllo di sistemi ibridi, una classe di sistemi dinamici caratterizzati da dinamiche continue e discrete tra di loro accoppiate, le quali descrivono tipicamente sistemi che sono composti da componenti fisiche e logiche e che appaiono in svariati contesti applicativi. L'idea è di sviluppare, attraverso un inquadramento teorico unificato, una collezione di approcci computazionali che operano su insiemi, svolgendo analisi di raggiungibilità ed invarianza in modo da stabilire se un dato sistema ibrido è in grado di soddisfare una certa proprietà relativa all'evoluzione del suo stato e di operare in modo sicuro e/o efficiente. Si considera il caso in cui l'evoluzione del sistema è soggetta a variabili di ingresso, le quali possono essere disturbi o variabili di controllo: se sono disponibili delle variabili di controllo, allora si sta affrontando un problema di controllo dove si vuole imporre un determinato comportamento a prescindere dall'incertezza che è presente sul sistema; se invece non ci sono variabili di controllo disponibili, allora, si sta considerando un problema di verifica. La tipologia di modelli considerata è quella dei sistemi dinamici affini a tratti (PWA) a tempo discreto, i quali sono sistemi ibridi caratterizzati da una partizione in poliedri dello spazio di stato continuo e da una collezione di dinamiche affini, ciascuna associata ad un elemento della partizione (chiamato modo) che rappresenta la componente discreta dello stato. I sistemi PWA sono in effetti equivalenti ad alcune classi di sistemi ibridi e possono astrarre le dinamiche non lineari lisce che descrivono l'evoluzione dello stato continuo in un sistema ibrido. L'insieme di tecniche computazionali qui sviluppate è ispirato da alcuni approcci già esistenti in letteratura relativi all'analisi di raggiungibilità, al problema di rappresentare gli insiemi di raggiungibilità adottando possibilmente delle tecniche di riduzione, e al calcolo di insiemi invarianti. Tali approcci vengono qui ulteriormente estesi e combinati tra di loro in un contesto unificato, che include anche il caso di incertezza parametrica tempo-variante, favorendo ulteriormente l'applicabilità delle tecniche basate su modello per la verifica e il controllo di sistemi PWA.