ReLU Barrier Functions for Nonlinear Systems with Constrained Control: A Union of Invariant Sets Approach

Titolo

Funzioni di Barriera ReLU per Sistemi Non Lineari con Vincoli di Controllo: Un Approccio basato sull'Unione di Insiemi Invarianti

1. Il Problema

La certificazione della sicurezza per sistemi dinamici non lineari soggetti a vincoli di ingresso poliedrici (saturazione) rappresenta una sfida significativa. I metodi tradizionali basati sulle Funzioni di Barriera di Controllo (CBF) incontrano due ostacoli principali:

1. Vincoli di ingresso: La saturazione dell'input può eliminare i controlli ammissibili necessari per mantenere la sicurezza, rendendo difficile la sintesi di una CBF valida.
2. Conservatorismo vs. Tracciabilità: La scelta della funzione di classe-$\mathcal{K}$ estesa $\alpha(\cdot)$ è critica. Scelte lineari permettono programmi convessi (facili da risolvere) ma spesso producono insiemi invarianti certificati molto piccoli (conservativi). Al contrario, funzioni non lineari potrebbero offrire insiemi più grandi, ma introducono non convessità che rendono il problema di ottimizzazione intrattabile o richiedono addestramento di reti neurali costoso e difficile da verificare.

L'obiettivo è sintetizzare una CBF per sistemi non lineari con vincoli di ingresso che riduca il conservatorismo senza sacrificare la tracciabilità computazionale (ovvero mantenendo la convessità dell'ottimizzazione).

2. Metodologia

Gli autori propongono una pipeline di approssimazione-verifica che combina sintesi convessa su modelli surrogati con verifica rigorosa sul sistema originale. Il metodo si articola in cinque fasi:

1. Approssimazione: I dinamismi non lineari a ciclo chiuso (con un controllo di riferimento fissato) sono approssimati da un modello Piecewise Affine (PWA) derivato da una rete neurale ReLU.
2. Sintesi (Surrogato): Viene sintetizzata una funzione di barriera PWA per il modello surrogato risolvendo un problema di Programmazione Lineare (LP).
   • Innovazione su $\alpha(\cdot)$: Invece di usare una funzione lineare fissa, viene proposta una funzione Leaky ReLU a due pendenze come surrogato per $\alpha(\cdot)$. Questo approccio evita la non convessità bilineare, permettendo di modellare comportamenti non lineari mantenendo la struttura LP.
3. Ampliamento (UIS): Per ridurre ulteriormente il conservatorismo, viene introdotta l'Unione di Insiemi Invarianti (Union of Invariant Sets - UIS).
   • Invece di selezionare il miglior singolo insieme ottenuto con un parametro $\alpha$, il metodo risolve il problema LP per una serie di parametri lineari diversi.
   • Gli insiemi invarianti risultanti sono uniti tramite una composizione max delle funzioni di barriera corrispondenti.
   • Teoricamente, l'insieme risultante è garantito essere invariante e non è mai più piccolo del miglior singolo insieme ottenuto con un $\alpha$ lineare, senza costi di ottimizzazione aggiuntivi.
4. Verifica (Faccia per Faccia): La CBF sintetizzata sul modello PWA viene verificata sul sistema non lineare originale.
   • Poiché la funzione di barriera è PWA, il suo insieme di livello zero (il confine) può essere decomposto in "patch" facciali.
   • La verifica viene eseguita su ciascuna patch utilizzando il Lemma di Farkas per eliminare la variabile di controllo $u$ e verificare l'esistenza di un controllo ammissibile che soddisfi la condizione di sicurezza.
5. Aggiornamento dell'Incertezza Locale: Se la verifica fallisce (viene trovato un controesempio), invece di ri-addestrare il modello globale, viene calcolato l'errore locale tra il modello reale e il surrogato in quel punto. Viene aggiunto un set di incertezza locale $\Delta_j$ solo alla cella interessata e il programma LP viene risolto nuovamente. Questo approccio evita di rendere l'intero problema eccessivamente conservativo.

3. Contributi Chiave

1. Surrogato Leaky ReLU per $\alpha(\cdot)$: Un design a due pendenze che bilancia la flessibilità non lineare con la tracciabilità della sintesi convessa, evitando la complessità delle funzioni $\mathcal{K}_\infty$ arbitrarie.
2. Unione di Insiemi Invarianti (UIS): Un metodo che combina certificati multipli basati su LP attraverso una composizione max. Garantisce un'area certificata più ampia rispetto alla scelta di un singolo $\alpha$ lineare, senza costi computazionali aggiuntivi significativi rispetto alla scansione multipla di $\alpha$.
3. Pipeline di Verifica Robusta: Un meccanismo che trasferisce le garanzie dal modello surrogato PWA al sistema non lineare originale tramite verifica facciale e aggiornamenti locali dell'incertezza, gestendo efficacemente la discrepanza del modello.

4. Risultati

Le simulazioni sono state condotte su sistemi classici con vincoli di saturazione:

• Pendolo Invertito: Il metodo UIS ha prodotto un insieme invariante certificato più grande rispetto ai progetti basati su $\alpha$ lineare singolo, con tempi di calcolo gestibili.
• Verifica del Certificato di Barriera (Sistema Non Lineare Generico): Confrontato con metodi basati su SOS (Sum of Squares) e reti neurali profonde, l'approccio proposto ha ottenuto un'area di copertura sicura paragonabile o superiore, utilizzando un modello ReLU molto più compatto (20 neuroni contro 256+ strati) e tempi di certificazione drasticamente inferiori (80 secondi contro centinaia di secondi o ore).
• Cart-Pole (4D): Il framework è stato scalato con successo a un sistema non lineare a 4 dimensioni con saturazione dell'input, dimostrando la capacità di gestire dinamiche complesse mantenendo la tracciabilità.

5. Significato e Impatto

Questo lavoro rappresenta un avanzamento significativo nella sicurezza formale dei sistemi di controllo:

• Superamento del Conservatorismo: Dimostra che è possibile ottenere insiemi di sicurezza molto più ampi rispetto ai metodi lineari tradizionali, sfruttando la flessibilità delle funzioni a pendenza multipla e l'unione di insiemi.
• Tracciabilità Computazionale: Mantiene la sintesi come un problema di Programmazione Lineare (convesso), rendendo il metodo scalabile e adatto a sistemi in tempo reale, a differenza di approcci basati su addestramento non convesso di reti neurali.
• Robustezza: La strategia di verifica e aggiornamento locale dell'incertezza garantisce che le certificazioni siano valide per il sistema fisico reale, non solo per il modello approssimato, colmando il divario tra teoria e pratica nei sistemi con vincoli di ingresso.

In sintesi, il paper offre un framework pratico ed efficiente per garantire la sicurezza di sistemi robotici e autonomi complessi in presenza di limitazioni fisiche degli attuatori.