Robust Verification of Controllers under State Uncertainty via Hamilton-Jacobi Reachability Analysis

Titolo

Verifica Robusta dei Controller in Presenza di Incertezza di Stato tramite Analisi di Raggiungibilità Hamilton-Jacobi

1. Il Problema

Con la crescente adozione di controller basati sulla percezione (spesso implementati con Reti Neurali - NN) per sistemi autonomi, diventa cruciale garantire formalmente la sicurezza e le prestazioni nonostante l'incertezza percettiva. L'incertezza può derivare da rumore nei sensori, errori di apprendimento nei moduli basati su ML o fattori ambientali (es. perdita del segnale GPS).

Le sfide principali identificate sono:

• Complessità dei Controller: I controller sono spesso non lineari, non convessi, basati su apprendimento automatico e/o "black-box".
• Limitazioni dei Metodi Esistenti: Le tecniche di verifica precedenti si basano su metodi di raggiungibilità approssimati (insiemi di iper-rettangoli, poliedri, zonotopi, ecc.). Questi metodi tendono a essere eccessivamente conservativi, portando spesso al fallimento nella certificazione della sicurezza, oppure sono limitati a classi specifiche di sistemi.
• Mancanza di Strumenti Formali: Non esisteva un framework basato su analisi di raggiungibilità formale (Hamilton-Jacobi) capace di gestire direttamente l'incertezza percettiva in sistemi a ciclo chiuso.

2. Metodologia: RoVer-CoRe

Gli autori propongono RoVer-CoRe (Robust Verification of Controllers via HJ Reachability), il primo framework basato sull'analisi di raggiungibilità Hamilton-Jacobi (HJ) per verificare sistemi basati sulla percezione sotto incertezza percettiva.

Astrazione del Sistema a Ciclo Chiuso

L'idea centrale è concatenare il controller, la funzione di osservazione e il modulo di stima dello stato per ottenere un sistema dinamico equivalente a ciclo chiuso.

• Modello: Il sistema è descritto da $\dot{x} = f(x, u, d)$, dove $u = \pi(q(p(x), e))$.
  • $x$: stato reale.
  • $p(x)$: osservazione (es. immagine).
  • $e$: errore percettivo (incertezza).
  • $q$: stimatore (es. filtro o NN).
  • $\pi$: controller basato sullo stato stimato $\hat{x}$.
• Trattamento dell'Incertezza: Sia il segnale di disturbo $d$ che il segnale di errore percettivo $e$ sono trattati come input avversi. Il sistema risultante ha come unici input esterni $d$ e $e$.

Calcolo dell'Hamiltoniano a Ciclo Chiuso

La sfida tecnica principale è calcolare l'Hamiltoniano del sistema a ciclo chiuso, che diventa una funzione non convessa di $d$ e $e$ a causa della complessità di $\pi, p, q$.
$$H(x, t, \nabla V) = \min_{d \in D, e \in E} \nabla V(x, t) \cdot h(x, d, e)$$
Per risolvere questo, RoVer-CoRe propone due approcci:

1. Calcolo Esatto: Se il controller è semplice o enumerabile (es. controllo MPC su griglia), l'ottimizzazione può essere risolta esattamente, fornendo garanzie non conservate.
2. Limitazione Inferiore (Lower Bounding): Per controller complessi (es. NN), si calcolano limiti inferiori e superiori sull'output del controller $\pi$ dato un errore percettivo limitato ($\hat{U}(x) \leq \pi(\hat{x}) \leq \bar{U}(x)$). Si utilizza quindi un insieme di controllo robusto $\mathcal{U}(x)$ per limitare inferiormente l'Hamiltoniano. Questo approccio è conservativo ma sound (garantisce che se il sistema è sicuro nel modello approssimato, lo è anche nel sistema reale).

Verifica e Progettazione Robusta

• Verifica di Sicurezza: Si calcola il "Backward Reachable Tube" (BRT), ovvero l'insieme degli stati iniziali da cui il sistema può essere forzato a entrare in un insieme di fallimento $F$ (es. collisione) sotto il peggior caso di disturbo ed errore. Se lo stato iniziale è fuori dal BRT, la sicurezza è garantita.
• Design del Controller: Il framework supporta l'ottimizzazione degli iperparametri. Si può cercare la configurazione del controller che massimizza il margine di sicurezza o il volume dell'insieme sicuro.

3. Risultati e Casi di Studio

Il framework è stato validato su due casi di studio reali:

A. Taxiing di un Aereo (Aircraft Taxiing)

• Scenario: Un aereo segue una linea centrale usando immagini di una telecamera alari. Un DNN stima l'errore di corsia e di assetto.
• Risultati:
  • RoVer-CoRe ha verificato formalmente la sicurezza fino a una copertura dell'errore del 99,68%.
  • Ha identificato controller "non sicuri" (quelli con guadagni eccessivi) che porterebbero all'uscita dalla pista in caso di errori percettivi.
  • Ha permesso di ottimizzare i guadagni del controller per garantire la sicurezza anche sotto incertezza massima.

B. Navigazione di un Rover Lunare (NN-Based Rover Navigation)

• Scenario: Un rover NASA naviga in condizioni di scarsa illuminazione (notte lunare). L'errore di odometria visiva cresce nel tempo se i fari sono spenti. Accendere i fari riduce l'errore ma consuma energia.
• Risultati:
  • Confronto tra un controller MPC (basato su griglia) e un NN che imita l'MPC.
  • RoVer-CoRe ha dimostrato che il BRT del NN è più "gonfiato" (più conservativo) rispetto all'MPC a causa degli errori di imitazione e dei limiti degli strumenti di verifica NN (α,β-CROWN), fornendo comunque una garanzia di sicurezza solida.
  • Design della Politica dei Fari: Il framework ha permesso di derivare una politica che accende i fari solo quando necessario (quando l'incertezza crescente minaccia di portare il rover nel BRT), garantendo la sicurezza e risparmiando energia.
  • Efficienza: RoVer-CoRe è risultato significativamente più preciso e completo rispetto a metodi Monte Carlo e allo strumento di verifica basato su insiemi NNV 2.0.

4. Contributi Chiave

1. RoVer-CoRe: Il primo framework basato su HJ reachability per la verifica formale di sistemi basati sulla percezione sotto incertezza.
2. Nuovi Metodi di Verifica: Tecniche per calcolare o limitare l'Hamiltoniano a ciclo chiuso, gestendo sia controller semplici che complessi (NN).
3. Design Robusto: Capacità di utilizzare i risultati di verifica per ottimizzare i parametri del controller e progettare politiche di gestione dell'incertezza (es. accensione fari).
4. Open Source: Il codice è stato reso disponibile pubblicamente.

5. Significato e Impatto

Questo lavoro colma un divario critico tra la teoria del controllo robusto (HJ reachability) e l'applicazione pratica dei sistemi autonomi basati su deep learning.

• Rigore: Offre garanzie formali di sicurezza che superano la conservatività dei metodi basati su approssimazione di insiemi.
• Praticità: Dimostra come la verifica formale possa guidare attivamente la progettazione di controller più sicuri ed efficienti, non limitandosi solo all'analisi a posteriori.
• Scalabilità: Sebbene l'analisi HJ sia computazionalmente costosa, l'uso di GPU e la capacità di gestire sistemi non lineari generali lo rendono un approccio promettente per sistemi critici come quelli aerospaziali e robotici.

In sintesi, RoVer-CoRe trasforma l'incertezza percettiva da un ostacolo intrattabile in una variabile gestibile all'interno di un quadro matematico rigoroso, permettendo di certificare la sicurezza di sistemi autonomi complessi in scenari reali.