Automatic verification and input design for dynamical systems: an optimization-based approach to the detection of non-inflential inputs

As the complexity of control systems grows, the verification of their correct functioning assumes a more important role. In the testing phase, when the system is checked against possible misbehaviors, the verification task consists in computing the input sequence to be injected in the system so as to generate that undesired behavior. When such an inputs sequence is found, the cause of the malfunctioning can be understood and the design of the control system improved accordingly. Nonetheless, it may happen that the detected input sequence is too complicated to interpret, since, for example, it requires to simultaneously set too many inputs. This prompts the need for novel verification methods, that provide "minimal" inputs sequences that satisfy a given specification (i.e., the misbehavior in the considered testing framework). In this work we address this need and develop techniques for the maximization of the number of non-influential inputs, i.e., those inputs that can take an arbitrary value in their range without compromising the satisfaction of the specification. We address this problem for the class of discrete time linear systems and discrete time Piecewise Affine (PWA) systems, in the case of reachability and safety specifications. For linear systems we develop two different techniques. In the first technique we rely on an input parametrization that treats the inputs as set valued signals and formulate a linear optimization problem with the objective of maximizing the range on where each input can vary, with the constraint on the satisfaction of the specification. In the second technique, we rely on a parametrization that allows the influential inputs to depend on the non-influential ones and formulate a Mixed Integer Linear Programming (MILP) problem with the objective of maximizing the number of non-influential inputs while enforcing the specification. As for the PWA case, we start by showing that an approach based on the extension of the first technique developed for the linear case leads to too conservative results. Prompted by the analysis of conservativeness, we reinterpret the problem from a geometrical perspective and formulate an exact approach to its solution, that, however, turns out to be intractable. On the base of this, we then construct an approximation of the exact problem that, despite being still conservative, leads to better results than the approach inspired by the linear case. As the approaches formulated for the PWA case can be computationally demanding, we also show, in the last part of this work, how to reduce their complexity via suitable techniques. In one of these techniques we show how to construct a reduced order PWA that preserves the input/output behavior of the original system by performing an extension of the classical observability analysis of linear systems.

All'aumentare della complessità dei sistemi di controllo, la verifica del loro corretto funzionamento assume un ruolo via via maggiore. Durante la fase di testing, quando si desidera assodare se il sistema mostra qualche comportamento indesiderato, il processo di verifica consiste nel calcolare le sequenze di ingresso che generano tale comportamento. Una volta che tale sequenza di ingresso è stata trovata, la causa del comportamento non desiderato può essere più facilmente compresa e, eventualmente, eliminata. Può tuttavia succedere che la sequenza di ingresso trovata sia eccessivamente complessa e difficile da interpretare; è il caso, ad esempio, di una sequenza che richieda di settare contemporaneamente un elevato numero di ingressi. Per questo motivo è necessario studiare tecniche che forniscano la "minima" sequenza di ingresso che rende soddisfatta una determinata specifica (che può essere ad esempio il comportamento non desiderato di cui sopra). A tal proposito in questo lavoro sviluppiamo delle tecniche per la massimizzazione del numero degli ingressi non-influenti, ovvero quegli ingressi che possono assumere un andamento arbitrario nel loro range, senza compromettere il soddisfacimento della specifica. Affrontiamo questo problema nella classe dei sistemi lineari a tempo discreto e nella classe dei sistemi affini a tratti (PieceWise Affine, PWA) a tempo discreto, nel caso di specifiche di raggiungibilità e safety. Nel caso lineare sviluppiamo due tecniche. Nella prima, parametrizziamo gli ingressi come funzioni a valori in un insieme e formuliamo un problema di ottimizzazione lineare con l'obiettivo di massimizzare il range su cui ciascun ingresso può variare e il vincolo di soddisfacimento della specifica. Nella seconda tecnica, utilizziamo una differente parametrizzazione che permette agli ingressi influenti di dipendere sui non-influenti e formuliamo un problema di ottimizzazione lineare mista intera con l'obiettivo di massimizzare il numero di ingressi non-influenti e al contempo soddisfare la specifica. Per quanto riguarda il caso PWA, mostriamo inizialmente che un approccio basato su un estensione della prima tecnica adottata nel caso lineare porta a risultati eccessivamente conservativi. Sulla base di questa considerazione, reinterpretiamo il problema da un punto di vista geometrico e formuliamo un approccio esatto che risulta tuttavia essere difficile da trattare. Formuliamo quindi una approssimazione della soluzione esatta che, nonostante ancora conservativa, permette di ottenere risultati migliori rispetto all'approccio ricavato dal caso lineare. Il problema che otteniamo è un problema di ottimizzazione mista intera che può essere computazionalmente oneroso; per questo motivo, nell'ultima parte di questo lavoro, mostriamo alcune tecniche utili a ridurne la complessità. In una di queste mostriamo che è possibile costruire un sistema PWA di ordine ridotto che preserva il comportamento ingresso/uscita del sistema originale attraverso un'estensione della classica analisi di osservabilità per sistemi lineari.