Safe and Robust Domains of Attraction for Discrete-Time Systems: A Set-Based Characterization and Certifiable Neural Network Estimation

Questo articolo propone un nuovo quadro teorico e computazionale basato su funzioni di valore definite su spazi metrici e reti neurali fisicamente informate, per la caratterizzazione precisa e la stima certificabile dei domini di attrazione sicuri e robusti per sistemi non lineari discreti incerti soggetti a vincoli di stato.

L'essenziale

Immagina di dover guidare un'auto su una strada di montagna molto tortuosa e scivolosa (il sistema incerto). Il tuo obiettivo è arrivare a una piccola piazzetta sicura in fondo alla valle (l'insieme stabile o RIS) senza mai uscire dalla carreggiata (i vincoli di sicurezza) e senza schiantarti, anche se il vento cambia direzione o la strada è ghiacciata in punti imprevisti (le incertezze).

La domanda è: Da quali punti di partenza posso essere sicuro al 100% di arrivare a quella piazzetta senza incidenti?

Questa è la domanda che il paper "Safe and Robust Domains of Attraction" cerca di rispondere, ma applicata a sistemi matematici complessi e computer. Ecco come funziona, spiegato con parole semplici e metafore.

1. Il Problema: La Mappa che non esiste

Fino ad ora, trovare questa "zona di partenza sicura" per sistemi complessi (come robot, reti elettriche o droni) era come cercare di disegnare una mappa di un labirinto mentre corri dentro di esso.

• I metodi vecchi: Usavano regole rigide (come cerchi perfetti o forme geometriche semplici) per disegnare la zona sicura. Il problema? Se il labirinto ha forme strane, queste regole rigide sono troppo conservative: ti dicono "non puoi partire da qui" anche se in realtà potresti farcela. È come dire che non puoi entrare in una stanza perché hai paura di sbattere la testa, anche se sei basso e la stanza è alta.
• Il problema dell'incertezza: Se c'è vento o ghiaccio (incertezze), i metodi vecchi spesso falliscono o diventano troppo cauti, restringendo inutilmente la zona sicura.

2. La Soluzione: Una "Bussola Intelligente" (La Rete Neurale)

Gli autori propongono un nuovo approccio che combina tre ingredienti magici:

A. La "Valuta" del Viaggio (Funzioni di Valore)

Immagina di avere una moneta speciale chiamata "Valuta di Pericolo".

• Se sei vicino alla piazzetta sicura, la moneta vale poco (pericolo basso).
• Se ti allontani o ti avvicini ai bordi della strada, la moneta vale sempre di più.
• Se esci dalla strada, la moneta vale infinito (pericolo assoluto).

L'obiettivo è calcolare quanto vale questa moneta per ogni punto della strada. Se la somma di tutte le monete che raccoglierai durante il viaggio è finita, sei al sicuro. Se è infinita, sei destinato a uscire dalla strada.

B. L'Allenamento con la "Fisica" (Physics-Informed Neural Networks)

Invece di far imparare a un'intelligenza artificiale (una Rete Neurale) solo guardando dati, gli autori gli insegnano le leggi della fisica del sistema.

• Immagina di addestrare un pilota simulato. Non gli dai solo foto della strada, ma gli dici: "Se giri qui con questo vento, l'auto scivolerà in quel modo".
• La rete neurale impara a prevedere la "Valuta di Pericolo" rispettando le regole matematiche del movimento (le equazioni di Bellman). In pratica, la rete impara a dire: "Se sono qui, e il vento soffia così, la mia prossima posizione sarà lì, e il mio livello di pericolo cambierà di questa quantità".

C. Il Controllore di Sicurezza (Verifica Formale)

Qui sta il vero trucco. Una rete neurale è brava a indovinare, ma può sbagliare. Come facciamo a essere sicuri che non ci stia mentendo?

• Dopo che la rete ha imparato a disegnare la mappa, usiamo un "Controllore di Sicurezza" (strumenti di verifica formale).
• È come un ispettore di sicurezza che prende la mappa disegnata dall'IA e la controlla rigorosamente punto per punto, usando la logica matematica pura, per assicurarsi che non ci siano buchi o errori. Se l'ispettore dice "OK", allora quella zona è certificata come sicura. Non è un'opinione, è un fatto matematico.

3. Perché è Geniale?

• Flessibilità: A differenza dei vecchi metodi che usavano cerchi rigidi, questo metodo può disegnare forme di sicurezza complesse e irregolari, adattandosi perfettamente alla forma reale della strada sicura.
• Robustezza: Funziona anche se c'è vento, pioggia o guasti (incertezze). La rete neurale è addestrata a considerare il "peggiore scenario possibile" durante l'apprendimento.
• Sicurezza Certificata: Non ci si fida ciecamente dell'IA. Si usa l'IA per trovare la soluzione e la matematica rigorosa per certificarla.

In Sintesi

Gli autori hanno creato un sistema che:

1. Impara a prevedere quanto è pericoloso un punto di partenza usando una rete neurale addestrata sulle leggi della fisica.
2. Disegna una mappa della zona sicura che si adatta perfettamente alla forma reale del problema (anche se è molto strana).
3. Verifica matematicamente che questa mappa sia corretta al 100%, garantendo che nessun sistema, nemmeno sotto stress o guasti, uscirà mai dai confini di sicurezza.

È come avere un GPS che non solo ti dice la strada migliore, ma ti garantisce matematicamente che, anche se piove o c'è traffico, non uscirai mai dalla carreggiata.

Sommario tecnico

1. Il Problema

Il lavoro affronta la sfida di stimare i Domini di Attrazione (DOA) per sistemi dinamici non lineari discreti soggetti a incertezze. Nello specifico, l'obiettivo è caratterizzare il DOA sicuro e robusto associato a un insieme attrattivo robusto invariante (RIS - Robust Invariant Set).

Un DOA sicuro e robusto è definito come l'insieme degli stati iniziali da cui tutte le traiettorie del sistema:

1. Convergono asintoticamente al RIS.
2. Rimangono all'interno di un insieme di stati sicuri (vincoli di stato) per tutti i tempi futuri.
3. Soddisfano queste condizioni per ogni possibile sequenza di disturbi ammissibili.

Le difficoltà principali risiedono nella natura non lineare del sistema, nella presenza di incertezze (disturbi), nei vincoli di stato e nella necessità di fornire garanzie formali (certificabilità) sulle stime ottenute, evitando le approssimazioni conservative tipiche dei metodi basati su funzioni di Lyapunov fisse.

2. Metodologia

L'approccio proposto integra tre componenti fondamentali: una caratterizzazione teorica basata su insiemi, l'approssimazione tramite reti neurali e la verifica formale.

A. Caratterizzazione Teorica: Funzioni di Valore su Spazi Metrici

Gli autori introducono nuove funzioni di valore definite su spazi metrici di insiemi compatti (spazi di Hausdorff).

• Stabilità $\ell_p$ uniforme: Il framework si basa sull'assunzione che il RIS sia uniformemente localmente $\ell_p$-stabile. Questa è una condizione generale che include la stabilità esponenziale e polinomiale come casi particolari.
• Definizione delle Funzioni: Vengono definite due funzioni di valore, $V$ e $W$, che caratterizzano esattamente il DOA sicuro e robusto.
  • $V(X)$ è la somma infinita di un termine di costo $\Psi$ calcolato sugli insiemi raggiungibili $R(X, k)$.
  • $W(X) = 1 - \exp(-V(X))$ è una trasformazione che mappa il dominio in un intervallo limitato $[0, 1)$.
• Equazioni di Bellman (Zubov-type): È dimostrato che queste funzioni sono le uniche soluzioni di equazioni funzionali di tipo Bellman:
  • $V(X) = \Psi(X) + V(F(X))$
  • $W(X) - W(F(X)) = \xi(X)(1 - W(F(X)))$
    dove $F(X)$ rappresenta l'immagine dell'insieme $X$ sotto la dinamica incerta.
• Proprietà: Le funzioni sono dimostrate essere funzioni di Lyapunov robuste, continue e uniche sotto specifiche condizioni di limite.

B. Apprendimento Fisico-Informato (Physics-Informed Neural Networks - PINN)

Per approssimare queste funzioni di valore in spazi ad alta dimensionalità, viene utilizzato un framework di reti neurali (NN).

• Embedding degli Insiemi: Poiché le equazioni di Bellman coinvolgono insiemi (non solo punti), viene introdotto un embedding $T$ che mappa insiemi compatti (come i singoli stati $\{x\}$ e gli insiemi raggiungibili $F(\{x\})$) in spazi vettoriali finiti $\mathbb{R}^L$. Questo permette di trattare l'incertezza come parte dell'input della rete.
• Funzione di Perdita: L'addestramento della rete neurale minimizza una funzione di perdita composta da:
  1. Termine Data-Driven: Minimizza la differenza tra l'output della rete e un'approssimazione a orizzonte finito della funzione di valore vera (calcolata tramite simulazione di traiettorie).
  2. Termine Fisico-Informato: Penalizza la violazione dell'equazione di Bellman (Zubov) durante l'addestramento. Questo vincola la rete a rispettare la dinamica del sistema e la struttura della stabilità.

C. Verifica Formale e Certificazione

L'approssimazione neurale da sola non garantisce la correttezza formale a causa degli errori di approssimazione. Per ovviare a ciò, viene proposto un protocollo di verifica:

1. Stima Iniziale: Si parte da un piccolo ROA (Region of Attraction) sicuro, spesso ottenuto tramite funzioni di Lyapunov quadratiche classiche.
2. Ampliamento Verificato: Utilizzando strumenti di verifica formale (come $\alpha,\beta$-CROWN o dReal), si verifica se le condizioni di invarianza e decrescita della funzione neurale sono soddisfatte su regioni più ampie.
3. Algoritmo: Si cercano i massimi livelli di soglia ($c_2, \omega_1, \omega_2$) tali che le condizioni di sicurezza e stabilità siano formalmente verificate per tutti i disturbi possibili. Questo trasforma l'approssimazione neurale in una stima del DOA certificata.

3. Contributi Chiave

1. Caratterizzazione Teorica Rigorosa: Introduzione di funzioni di valore su spazi di insiemi compatti che caratterizzano esattamente il DOA sicuro e robusto per sistemi discreti non lineari, rilassando molte assunzioni tecniche presenti nella letteratura precedente (es. continuità Lipschitz locale, limitatezza dell'insieme sicuro).
2. Equazioni di Bellman per Sistemi Incerti: Derivazione di equazioni funzionali di tipo Zubov/Bellman adattate per la dinamica incerta e i vincoli di stato, che fungono da base per l'apprendimento.
3. Framework Ibrido NN-Verifica: Sviluppo di un metodo che combina l'efficienza e la flessibilità delle reti neurali (per l'approssimazione in alta dimensione) con la rigore della verifica formale (per garantire la sicurezza).
4. Generalità: Il metodo non è limitato a sistemi polinomiali (a differenza dei metodi SOS) e gestisce insiemi di disturbo compatti e generici, non solo punti di equilibrio.

4. Risultati Sperimentali

Il metodo è stato validato su quattro esempi numerici, inclusi sistemi di potenza, sistemi non lineari con stabilità polinomiale e un sistema meccanico (asta rigida).

• Confronto: I risultati sono stati confrontati con:
  • Metodi basati su ellissoidi ottimizzati (Lyapunov quadratici).
  • Reti neurali addestrate su dinamica nominale (senza incertezza).
  • Metodi basati su funzioni di Lyapunov dipendenti dai parametri.
• Prestazioni:
  • In presenza di disturbi (Scenario 2), il metodo proposto ha fornito le stime del DOA più ampie e certificabili.
  • Le reti neurali addestrate solo sulla dinamica nominale hanno fallito nel produrre stime certificabili per diversi esempi quando l'incertezza era attiva.
  • Il metodo proposto ha superato i metodi basati su ellissoidi, dimostrando di poter catturare geometrie del DOA non convesso e complesse.
• Efficienza: I tempi di calcolo per l'addestramento e la verifica sono risultati competitivi, sebbene la generazione dei dati (calcolo degli insiemi raggiungibili) rappresenti il collo di bottiglia computazionale, come previsto per i metodi basati su simulazione.

5. Significato e Impatto

Questo lavoro rappresenta un avanzamento significativo nella teoria del controllo robusto e nell'apprendimento automatico per sistemi dinamici:

• Superamento delle limitazioni dei metodi classici: Offre una soluzione scalabile per sistemi non lineari complessi dove i metodi analitici o polinomiali (SOS) falliscono o sono troppo conservativi.
• Garanzie di Sicurezza: Risolve il problema della "scatola nera" delle reti neurali nel controllo critico, fornendo un meccanismo per trasformare un'approssimazione neurale in un certificato di sicurezza matematico.
• Versatilità: La capacità di gestire insiemi di disturbo compatti e vincoli di stato rende il framework applicabile a scenari reali complessi, come la robotica, i sistemi di potenza e il controllo di veicoli autonomi in ambienti incerti.

In sintesi, il paper propone un ponte teorico e pratico tra la teoria della stabilità robusta classica e le moderne tecniche di apprendimento profondo, garantendo che le prestazioni ottenute siano non solo accurate, ma anche formalmente sicure.