An Update to the Level Set Theorems in Hamilton-Jacobi Reachability Analysis

Sintesi Tecnica: Un aggiornamento ai Teoremi di Livello di Insieme nella Analisi di Raggiungibilità Hamilton-Jacobi

Definizione del Problema
La Raggiungibilità Hamilton-Jacobi (HJR) è un framework consolidato per la sintesi di controllori per sistemi non lineari critici per la sicurezza sotto incertezza, tipicamente formulata come giochi differenziali. Il processo prevede la conversione di un compito di controllo qualitativo (ad esempio, l'evitamento di ostacoli o il raggiungimento di un obiettivo) in un "gioco di grado", risolvendo l'equazione alle derivate parziali di Hamilton-Jacobi (HJ) associata per ottenere una funzione valore e, infine, interpretando tale funzione valore per definire l'insieme di stati iniziali sicuri o non sicuri. Questo passaggio finale si basa sui "Teoremi di Livello di Insieme" (Level Set Theorems).

Gli autori identificano che la letteratura esistente contiene errori tecnici e ambiguità riguardo a questi teoremi, specificamente concernenti le condizioni sotto le quali i livelli di insieme della funzione valore corrispondono correttamente agli insiemi vincenti del gioco. Tali problematiche hanno causato confusione nella comunità, in particolare riguardo all'interpretazione degli stati che giacciono esattamente sul livello zero della funzione valore. Il documento sostiene che le formulazioni precedenti spesso trascurano assunzioni topologiche e di convessità necessarie, portando a caratterizzazioni errate dei set di sicurezza e di raggiungibilità.

Metodologia
Il documento impiega un approccio matematico rigoroso radicato nella teoria dei giochi differenziali e nella topologia. Gli autori:

1. Formalizzano l'impostazione del Gioco: Definiscono un gioco differenziale a orizzonte finito con un giocatore controllore e un giocatore disturbo avversario. La dinamica del sistema è governata da $\dot{x} = f(x, a, b)$, dove $a$ e $b$ sono rispettivamente segnali di controllo e di disturbo. Il giocatore disturbo utilizza strategie non anticipative.
2. Stabiliscono le Assunzioni: L'analisi si basa su cinque assunzioni chiave:
   • Continuità standard e compattezza delle dinamiche e dei set di controllo (Assunzioni 1-3).
   • Convessità delle dinamiche di disturbo: Per ogni stato e controllo, l'insieme dei possibili vettori di dinamica indotti dal set di disturbo $B$ deve essere convesso (Assunzione 4).
   • Chiusezza dei modi di fallimento: L'insieme delle traiettorie di fallimento $F(t)$ deve essere chiuso nello spazio delle traiettorie continue (Assunzione 5).
3. Derivano un Teorema Generale: Dimostrano un teorema generalizzato del Livello di Insieme (Teorema 1) che collega la funzione valore $v(x,t)$ agli insiemi sicuri ($L(t)$) e non sicuri ($G(t)$). Il teorema stabilisce che $L(t) = \{x \mid v(x,t) > 0\}$ e $G(t) = \{x \mid v(x,t) \leq 0\}$, a condizione che il funzionale $J$ che definisce i modi di fallimento sia continuo e limitato.
4. Costruiscono Controesempi: Per dimostrare la necessità delle nuove assunzioni, gli autori costruiscono due specifici controesempi:
   • Mancanza di Convessità: Un gioco di evitamento ostacoli in cui il set di disturbo $B$ è non convesso (punti discreti). Dimostrano che, senza l'Assunzione 4, uno stato sul livello zero ($v=0$) potrebbe non appartenere all'insieme non sicuro, contraddicendo le interpretazioni standard.
   • Target Set Chiusi: Un gioco di raggiungimento obiettivo in cui il set target è chiuso anziché aperto. Dimostrano che, senza l'Assunzione 5 (che implica che i target debbano essere aperti), uno stato sul livello zero potrebbe non appartenere all'insieme sicuro, contraddicendo nuovamente le interpretazioni standard.
5. Tecniche di Dimostrazione: Le dimostrazioni utilizzano il Lemma di Filippov per stabilire l'esistenza di segnali di disturbo misurabili, e argomenti topologici riguardanti la compattezza dei set di traiettorie e i piani di disturbo non anticipativi (usando il Teorema di Tychonoff e l'ordinamento lessicografico) per provare il teorema principale.

Contributi Chiave

1. Correzione di Errori Tecnici: Il documento identifica e corregge difetti tecnici nei precedenti Teoremi di Livello di Insieme presenti in letteratura, puntando specificamente all'omissione della condizione di convessità sulle dinamiche (Assunzione 4) e al requisito di set di fallimento chiusi (Assunzione 5).
2. Teorema del Livello di Insieme Generale: Gli autori forniscono un teorema unificato e conciso applicabile a tutti i giochi a orizzonte finito di interesse nella HJR, chiarendo la disuguaglianza stretta per l'insieme sicuro ($v > 0$) e la disuguaglianza non stretta per l'insieme non sicuro ($v \leq 0$).
3. Chiarimento dell'Ambiguità del Livello Zero: Attraverso i controesempi, il documento spiega perché i punti sul livello zero della funzione valore siano ambigui quando le assunzioni standard vengono violate. In tali casi, l'esito del gioco (vittoria/sconfitta) per questi specifici punti non può essere determinato esclusivamente dal fatto che la funzione valore sia zero; il controllore può vincere per alcuni punti sul confine mentre il disturbo vince per altri.
4. Rigore Topologico: Il lavoro colma il divario tra la HJR e gli argomenti topologici utilizzati nella teoria della vitalità (viability theory) e nelle barriere semi-permeabili, offrendo una base teorica più robusta per l'interpretazione delle funzioni valore.

Risultati
Il risultato primario è il Teorema 1, che definisce rigorosamente gli insiemi sicuri e non sicuri basandosi sulla funzione valore sotto le specifiche assunzioni. Il documento dimostra che:

• Se le dinamiche di disturbo non sono convesse (ad esempio, set di disturbo discreti), l'interpretazione standard secondo cui $v(x,t) \leq 0$ implica che lo stato è non sicuro fallisce per i punti sul confine.
• Se il set target è chiuso (violando il requisito di target aperti nei giochi di raggiungibilità), l'interpretazione standard secondo cui $v(x,t) > 0$ implica che lo stato è sicuro fallisce per i punti sul confine.
• Sotto le assunzioni corrette, la funzione valore fornisce una caratterizzazione precisa degli insiemi vincenti, con il giocatore disturbo che detiene un "vantaggio istantaneo" che rende necessaria la divisione tra disuguaglianza stretta e non stretta.

Significatività
Gli autori affermano che, sebbene questi problemi tecnici possano non impattare immediatamente i praticanti che si affidano a strumenti software esistenti, la loro risoluzione teorica è "interessante e sfumata". Il documento mira a chiarire la confusione nella comunità causata da precedenti errori tecnici. Fornendo un teorema generale corretto e spiegando l'origine delle discrepanze tramite controesempi, il lavoro assicura che i fondamenti teorici della Raggiungibilità Hamilton-Jacobi siano solidi. Ciò è particolarmente rilevante per i ricercatori che sviluppano metodi HJR basati sull'apprendimento o che estendono il framework a compiti complessi e stratificati, poiché chiarisce le condizioni precise richieste affinché la funzione valore certifichi correttamente sicurezza e liveness.