An abstraction and refinement approach to safety analysis of nonlinear systems

This thesis addresses safety verification for a nonlinear system, based on invariant set computation. More precisely, we aim at verifying if the state of a discrete time nonlinear system will keep evolving within a safety region, starting from a given set of initial conditions. To this purpose, we develop a method based on abstraction and refinement to compute an approximation of the largest invariant set within the safety region. If such an approximation contains all initial conditions, then, safety is proven. The proposed method relies on the abstraction of the nonlinear system to a PieceWise Affine (PWA) model with an additive disturbance that accounts for the abstraction error. Given that all state trajectories of the nonlinear system are admissible for its abstraction, we can obtain an inner approximation of the invariant set of the original nonlinear system by computing the corresponding (robust) invariant set for its PWA abstraction. We adopt a PWA abstraction for two main reasons: (i) the universal approximation property of PWA functions with respect to smooth nonlinear functions guarantees that, by successively refining the PWA abstraction through a procedure satisfying the refinement inclusion property, we get an inner approximation of the actual invariant set that is more and more accurate; (ii) a computationally efficient method is available for determining polytopic robust invariant sets for PWA systems, through an iterative procedure that starts from a polytopic set covering the safe region and progressively reduces it while imposing the set invariance property. The idea is then to start from a rough PWA abstraction, check if the associated polytopic robust invariant set contains the set of initial conditions, and if this is not the case perform a refinement of the abstraction to get an improved approximation of the actual invariant set. The refinement can simply be performed uniformly on the safe region or be nested within the iterative procedure for polytopic robust invariant set computation for the current PWA abstraction. This latter variant leads to a guided refinement, which is computationally far more convenient than the former, as shown through some numerical examples.

Questo lavoro di tesi riguarda la verifica di safety di un sistema dinamico non lineare tramite il calcolo di insiemi invarianti. Nello specifico, si vuole stabilire se lo stato di un sistema non lineare a tempo discreto continuerà ad evolvere all'interno di una regione safe, a partire da un insieme preassegnato di condizioni iniziali. A tale scopo, si sviluppa un metodo basato su astrazione e raffinamento di modello per calcolare un'approssimante del massimo insieme invariante all'interno della regione safe. Se tale approssimante contiene tutte le possibili condizioni iniziali, allora la safety è verificata. Il metodo proposto si avvale di un'astrazione del sistema non lineare tramite un modello affine a tratti (PWA dall'acronimo inglese PieceWise Affine) soggetto ad un disturbo additivo che tiene conto dell'errore di approssimazione introdotto. Poiché le traiettorie dell'astrazione includono tutte quelle del sistema non lineare, si può ottenere un'approssimazione per difetto dell'insieme invariante d'interesse per il sistema originario calcolando il corrispondente invariante (robusto) per la sua astrazione PWA. L'impiego di un'astrazione PWA è motivato da due principali ragioni: (i) la proprietà delle funzioni PWA di essere approssimanti universali di funzioni nonlineari regolari garantisce che, tramite raffinamenti successivi dell'astrazione PWA mediante una procedura che soddisfi le proprietà di inclusione delle traiettorie delle astrazioni più fini all'interno dell'insieme delle traiettorie delle astrazioni più grezze, siamo in grado di ottenere un'approssimazione per difetto dell'effettivo insieme invariante gradualmente più accurata; (ii) per determinare l'invariante robusto per sistemi PWA, è disponibile un metodo computazionalmente efficiente che, a partire da un politopo che ricopre l'intera regione safe, lo riduce progressivamente tramite una procedura iterativa, imponendo ad ogni iterazione la proprietà di invarianza. L'idea è di partire da un'astrazione PWA grezza, verificare se il corrispondente invariante robusto politopico contiene l'insieme delle condizioni iniziali e, qualora ciò non avvenisse, raffinare l'astrazione per migliorare la qualità dell'approssimazione dell'invariante effettivo. La procedura di raffinamento può essere applicata in maniera uniforme all'interno della regione di safety, oppure essere integrata in quella di calcolo iterativo dell'invariante robusto politopico per l'astrazione PWA corrente. Questa seconda opzione si traduce in una procedura di raffinamento guidato, la quale risulta essere decisamente più conveniente della prima da un punto di vista computazionale, come mostrato nella tesi tramite alcuni esempi numerici.