Data-Driven Reachability of Nonlinear Lipschitz Systems via Koopman Operator Embeddings

Il paper propone un framework di raggiungibilità basato sull'operatore di Koopman e su rappresentazioni zonotopiche che, sollevando i sistemi non lineari in uno spazio lineare, permette di ottenere sovrastime più strette dei set raggiungibili rispetto ai metodi tradizionali, garantendo al contempo la verifica formale della sicurezza.

L'essenziale

Immagina di dover guidare un'auto a guida autonoma in una strada piena di curve, nebbia e imprevisti. Il tuo obiettivo è sapere con certezza: "Dove potrà arrivare l'auto nei prossimi 10 secondi, considerando che potrei sbagliare un po' di sterzata o che la strada è scivolosa?"

Questa è la sfida della sicurezza robotica. Se sbagliamo i calcoli, l'auto potrebbe finire contro un muro. Se i calcoli sono troppo "paranoici" (conservativi), l'auto si fermerà per paura di muoversi, bloccando il traffico.

Ecco di cosa parla questo articolo, spiegato come una storia:

1. Il Problema: La Mappa che non c'è

Di solito, per prevedere dove va un'auto, i programmatori usano un modello matematico perfetto (come una ricetta di cucina). Ma nel mondo reale, le ricette sono spesso sbagliate o incomplete.

• Il vecchio metodo: Usare una mappa approssimativa. Per essere sicuri di non sbattere, i vecchi metodi disegnavano un "cerchio di sicurezza" enorme intorno all'auto. È sicuro? Sì. Ma è così grande che l'auto sembra bloccata in una gabbia invisibile. È troppo conservativo.
• Il problema dei dati: Se proviamo a imparare guardando solo i dati (es. "l'auto ha fatto così 100 volte"), i metodi attuali tendono a diventare confusi e a disegnare cerchi di sicurezza ancora più grandi man mano che guardiamo più in là nel tempo.

2. La Soluzione Magica: Il "Trucco del Proiettore" (Operatore di Koopman)

Gli autori hanno trovato un modo geniale per aggirare il problema. Immagina che il movimento dell'auto sia come un film in 3D molto complicato. È difficile prevedere dove andrà il protagonista se seguiamo solo la sua posizione (x, y).

L'idea di questo articolo è usare un proiettore speciale (l'Operatore di Koopman).

• Invece di guardare il film in 3D, il proiettore lo "proietta" su uno schermo piatto (uno spazio matematico più grande).
• La magia: In questo nuovo mondo proiettato, il movimento complicato e curvo dell'auto diventa semplice e dritto, come se l'auto stesse andando in linea retta su un binario.
• Una volta che abbiamo previsto dove andrà l'auto in questo mondo "semplice", usiamo il proiettore al contrario per riportare la previsione nel mondo reale.

3. Come funziona in pratica?

Immagina di voler prevedere il percorso di un pallone che rimbalza in modo imprevedibile.

1. Guardiamo i dati: Prendiamo un mucchio di video di palloni che rimbalzano (i dati reali, anche se un po' sfocati o rumorosi).
2. Creiamo il "Ponte": Usiamo un algoritmo intelligente per trovare le regole matematiche che trasformano il movimento caotico in un movimento lineare. È come se dicessimo: "Ok, in questo mondo speciale, ogni volta che il pallone rimbalza, in realtà sta solo facendo un piccolo passo avanti".
3. Calcoliamo il percorso: Nel mondo speciale, è facilissimo calcolare dove finirà il pallone. Disegniamo un "tubo" (chiamato zonotopo, che è una forma geometrica intelligente) che racchiude tutte le possibilità.
4. Torniamo alla realtà: Proiettiamo quel tubo indietro nel mondo reale.
5. Il "Paracadute" di sicurezza: Sappiamo che il nostro proiettore non è perfetto. C'è sempre un piccolo errore. Quindi, aggiungiamo un piccolo "cuscinetto" o "paracadute" (chiamato residuo) intorno al tubo. Questo ci garantisce che, anche se il proiettore sbaglia un po', l'auto vera sarà comunque dentro il nostro tubo di sicurezza.

4. Perché è meglio degli altri?

• I vecchi metodi (Lineari): Sono come cercare di descrivere una curva usando solo linee rette. Per coprire la curva, devi disegnare un rettangolo enorme.
• I nuovi metodi (Koopman): Sono come usare un righello flessibile che si adatta alla curva. Il tubo di sicurezza è molto più stretto e preciso.
• Il risultato: L'auto può guidare più velocemente e più vicino agli ostacoli senza rischiare, perché il "cerchio di sicurezza" è più piccolo e più realistico.

5. La Prova sul Campo

Gli autori non si sono limitati a fare calcoli su carta. Hanno provato il loro metodo su:

1. Un reattore chimico (un sistema complesso che reagisce in modo non lineare).
2. Un'auto da corsa autonoma reale (un JetRacer) che correva in un laboratorio.

Il verdetto?
Il loro metodo ha disegnato percorsi di sicurezza molto più stretti e precisi rispetto a tutti gli altri metodi esistenti, specialmente quando guardavano in là nel tempo (orizzonti lunghi). È come se avessero sostituito una mappa disegnata a mano con un GPS satellitare ad alta precisione, permettendo all'auto di muoversi con più fiducia e meno paura.

In sintesi

Questo articolo ci dice: "Non serve conoscere la ricetta perfetta per prevedere il futuro. Se guardi abbastanza dati e usi il trucco giusto (Koopman) per semplificare la realtà, puoi disegnare confini di sicurezza così precisi da permettere ai robot di essere più audaci e sicuri allo stesso tempo."

Sommario tecnico

Titolo

Analisi di Raggiungibilità Basata sui Dati per Sistemi Non Lineari Lipschitziani tramite Incorporamenti dell'Operatore di Koopman

1. Il Problema

La verifica formale della sicurezza nei sistemi robotici richiede spesso l'analisi di raggiungibilità (reachability analysis) per determinare l'insieme di tutti gli stati futuri possibili dati un insieme di condizioni iniziali incerte e disturbi.

• Limiti degli approcci attuali: I metodi basati su modelli formali richiedono dinamiche di sistema precise, spesso difficili da ottenere per piattaforme complesse. I metodi data-driven esistenti, che utilizzano rappresentazioni zonotopiche per scalabilità ed efficienza, tendono a diventare eccessivamente conservativi (sovrastimano l'insieme raggiungibile) quando applicati a sistemi non lineari, specialmente su orizzonti temporali lunghi o in presenza di rumore di misura.
• Obiettivo: Sviluppare un framework data-driven che fornisca garanzie di sicurezza formali (sovra-approssimazioni garantite) per sistemi non lineari non affini, riducendo al contempo il conservatorismo rispetto ai metodi lineari tradizionali.

2. Metodologia Proposta

Il paper propone un framework che combina la teoria dell'operatore di Koopman con l'analisi di raggiungibilità basata su zonotopi.

A. Incorporamento di Koopman (Koopman Embedding)

Invece di modellare direttamente la non linearità nel spazio degli stati originale, il sistema viene "sollevato" (lifted) in uno spazio di osservabili a dimensione superiore.

• Dinamica Sollevata: L'operatore di Koopman trasforma le dinamiche non lineari in dinamiche lineari (o quasi-lineari) nello spazio degli osservabili.
• Funzioni di Sollevamento (Lifting Functions): Il metodo utilizza funzioni di sollevamento dipendenti sia dallo stato che dall'ingresso ($\phi(x_k)$ e $\nu(x_k, u_k)$). Questo è un miglioramento rispetto ai modelli LTI (Lineari Tempo-Invarianti) standard, permettendo una rappresentazione lineare più accurata di sistemi non affini.
• Identificazione dai Dati: L'operatore di Koopman (matrice $K$) viene identificato direttamente dai dati misurati (traiettorie stato-ingresso rumorose) utilizzando una regressione ai minimi quadrati (Least Squares).

B. Gestione degli Errori e del Rumore

Per garantire che l'analisi sia rigorosa e sicura, il framework quantifica e racchiude tutte le fonti di incertezza:

1. Rumore di Processo: Il rumore $w_k$ è modellato come uno zonotopo noto.
2. Errore di Linearizzazione: L'errore introdotto dall'approssimazione lineare delle dinamiche sollevate è calcolato e limitato.
3. Residuo di Modellazione (Koopman Residual): L'errore derivante dall'apprendimento dell'operatore dai dati (discrepanza tra il modello sollevato e le traiettorie reali) viene calcolato aggregando gli errori di previsione multi-step su tutte le traiettorie disponibili.
4. Copertura del Dataset: Viene utilizzato un raggio di copertura ($\delta$) e la costante di Lipschitz per estendere i limiti degli errori dal dataset osservato all'intero dominio raggiungibile.

C. Propagazione degli Insiemi Raggiungibili

1. Si calcolano gli insiemi raggiungibili nello spazio sollevato utilizzando la propagazione di zonotopi attraverso le dinamiche lineari identificate.
2. Gli insiemi vengono proiettati nuovamente nello spazio degli stati originale.
3. Si esegue la somma di Minkowski tra l'insieme proiettato e gli insiemi di incertezza derivanti (errore di modellazione, rumore, residuo) per ottenere una sovra-approssimazione garantita dell'insieme raggiungibile reale.

3. Contributi Chiave

• Framework Data-Driven per Sistemi Non Affini: Introduzione di un metodo per l'analisi di raggiungibilità di sistemi non lineari non affini (Lipschitziani) che gestisce direttamente dati rumorosi stato-ingresso.
• Sollevamento Stato-Ingresso Dipendente: Sviluppo di un approccio di identificazione che utilizza osservabili dipendenti sia dallo stato che dall'ingresso, migliorando l'accuratezza rispetto ai modelli LTI sollevati convenzionali.
• Garanzie Formali Rigorose: Dimostrazione matematica (Teorema 1) che gli insiemi raggiungibili calcolati costituiscono una sovra-approssimazione valida dell'insieme raggiungibile esatto, tenendo conto di rumore, errore di linearizzazione ed errore di identificazione dai dati.
• Efficienza Computazionale: Utilizzo di rappresentazioni zonotopiche che permettono calcoli efficienti (somme di Minkowski e trasformazioni lineari) mantenendo la scalabilità.

4. Risultati Sperimentali

Il metodo è stato validato su tre casi di studio:

1. Reattore Chimico (CSTR): Un sistema dinamico affine. Il metodo proposto ha mostrato una significativamente minore conservatività rispetto ai modelli basati su minimi quadrati (LS) e agli strumenti basati su modelli (CORA v2025), specialmente su orizzonti temporali lunghi.
2. Sistema Non Affine: Un sistema non lineare non affine complesso. Anche in questo caso, il metodo Koopman ha prodotto insiemi raggiungibili più stretti rispetto alle alternative, dimostrando la capacità di catturare dinamiche non lineari complesse.
3. Veicolo Autonomo (JetRacer): Esperimento su un robot da corsa reale con hardware embedded (NVIDIA Jetson Nano). I risultati reali hanno confermato che l'approccio proposto genera insiemi raggiungibili molto più precisi rispetto ai metodi data-driven lineari esistenti, riducendo l'area di incertezza senza perdere le garanzie di sicurezza.

5. Significato e Impatto

Questo lavoro colma un divario importante tra l'identificazione di sistemi basata sui dati e la verifica formale della sicurezza.

• Miglioramento della Sicurezza Operativa: Riducendo il conservatorismo, i robot possono operare più vicino ai limiti fisici reali senza violare i vincoli di sicurezza, migliorando l'efficienza operativa.
• Applicabilità Reale: La capacità di gestire sistemi non affini e rumore di misura direttamente dai dati rende il metodo adatto a scenari reali dove i modelli analitici sono inesistenti o imprecisi.
• Scalabilità: L'uso di zonotopi e della linearizzazione di Koopman permette di analizzare sistemi complessi su orizzonti temporali lunghi, un compito spesso proibitivo per i metodi non lineari diretti.

In sintesi, il paper presenta una soluzione robusta che trasforma l'analisi di raggiungibilità da un approccio puramente conservativo a uno più preciso e adattivo, mantenendo al contempo la certezza matematica necessaria per applicazioni critiche come la robotica autonoma.