On transferring safety certificates across dynamical systems

Titolo: Trasferimento di certificati di sicurezza attraverso sistemi dinamici

1. Il Problema

L'articolo affronta una sfida fondamentale nel controllo dei sistemi autonomi: la difficoltà di applicare direttamente le Funzioni di Barriera di Controllo (Control Barrier Functions - CBF) a sistemi fisici complessi e ad alta dimensionalità (come i droni quadrotor).

• Il divario modellistico: Le specifiche di sicurezza sono spesso progettate e verificate su modelli semplificati o astratti (es. integratori doppi) perché sono trattabili per la verifica formale. Tuttavia, quando queste garanzie vengono implementate su piattaforme fisiche reali, dinamiche non lineari, sottodimensionamento (underactuation) e limitazioni degli attuatori possono invalidare i certificati di sicurezza derivati dai modelli ideali.
• Limiti degli approcci esistenti: I metodi classici basati su relazioni di simulazione o bisimulazione approssimata sono utili per la verifica temporale logica, ma la loro applicazione alla sintesi di controllori di sicurezza critici tramite CBF è stata poco esplorata. I metodi attuali richiedono spesso la progettazione di funzioni barriera direttamente sul sistema non lineare completo, il che è computazionalmente proibitivo o richiede un'esperienza di dominio significativa.

2. Metodologia: Il Framework tCBF

Gli autori propongono un nuovo framework chiamato Control Barrier Function Trasferito (tCBF). L'obiettivo è trasferire formalmente le garanzie di sicurezza da un sistema astratto ($\Sigma_1$) a un sistema concreto più complesso ($\Sigma_2$) collegati da una funzione di simulazione.

I pilastri metodologici sono:

• Funzione di Simulazione ($V$): Una funzione che misura la discrepanza tra lo stato del sistema astratto e quello concreto, garantendo che il sistema concreto possa approssimare il comportamento di quello astratto entro un certo margine di errore.
• Mappa di Testimone (Witness Map - $\Pi$): Una mappa che, dato uno stato concreto $x_2$, trova lo stato astratto "più vicino" $x_1 = \Pi(x_2)$ minimizzando la funzione di simulazione $V$.
• Costruzione della Funzione Barriera Trasferita ($b_2$):
  La nuova funzione di barriera per il sistema concreto è definita come:
  $$b_2(x_2) := b_1(\Pi(x_2)) - \phi(V(\Pi(x_2), x_2))$$
  Dove:
  • $b_1$ è la CBF valida sul sistema astratto.
  • $\phi$ è una funzione di margine ($\phi \in \mathcal{K}_\infty$) progettata specificamente per compensare l'errore di simulazione e il disallineamento dinamico.
• Condizioni di Progettazione:
  Gli autori derivano condizioni sufficienti per la scelta della funzione di margine $\phi$. In particolare, $\phi$ deve crescere abbastanza velocemente da garantire che il decadimento della funzione di simulazione (che riduce l'errore) compensi sia la contrazione della barriera astratta sia qualsiasi residuo di disallineamento dinamico ($\delta$). Questo porta a un'equazione differenziale (o disuguaglianza) che definisce $\phi$.
• Filtro di Sicurezza QP:
  Una volta costruita $b_2$, la sicurezza viene imposta sul sistema concreto risolvendo in tempo reale un Programma Quadratico (QP). Questo filtro modifica minimamente un controllore nominale ($u_{nom}$) solo quando necessario per soddisfare la condizione di invarianza forward di $b_2$.

3. Contributi Chiave

1. Costruzione Formale tCBF: Introduzione di una formulazione matematica rigorosa che permette di trasferire certificati di sicurezza da modelli astratti a sistemi non lineari ad alta dimensionalità utilizzando funzioni di simulazione e margini espliciti.
2. Garanzie Formali e Linee Guida: Dimostrazione che, con una progettazione appropriata della funzione di margine, i certificati di sicurezza trasferiti sono validi per il nuovo sistema. Forniscono condizioni esplicite (inclusi casi a forma chiusa) per selezionare $\phi$ senza bisogno di ottimizzazione numerica esaustiva.
3. Decoupling Sintesi/Impostazione: Il framework permette di separare la sintesi della sicurezza (fatta su modelli semplici) dalla sua imposizione (sui sistemi complessi), rendendo il processo scalabile e adattabile a sistemi eterogenei.

4. Risultati Sperimentali

Il framework è stato validato su un caso d'uso di navigazione di un quadrotor in un ambiente 3D affollato di ostacoli.

• Setup:
  • Sistema Astratto ($\Sigma_1$): Un integratore doppio 3D (modello semplice).
  • Sistema Concreto ($\Sigma_2$): Dinamica completa del quadrotor (non lineare, sottodimensionato, con rotazioni SO(3)).
  • Obiettivo: Evitare collisioni con ostacoli sferici.
• Implementazione:
  • È stata utilizzata una funzione di simulazione basata sull'errore di posizione e velocità.
  • La funzione di margine $\phi$ è stata calcolata analiticamente in base alle condizioni teoriche.
  • Un controllore nominale (basato su pianificazione RRT* e ottimizzazione di traiettoria "minimum-snap") è stato filtrato dal modulo tCBF-QP.
• Risultati:
  • Evitamento Collisioni: Il quadrotor ha navigato con successo evitando tutti gli ostacoli, mantenendo una distanza geometrica strettamente positiva, nonostante le discrepanze tra il modello astratto e la realtà fisica.
  • Minima Invasività: Il filtro di sicurezza ha modificato la traiettoria nominale solo nelle vicinanze degli ostacoli. Lontano dalle zone critiche, il sistema ha seguito la traiettoria ottimizzata originale, preservando le prestazioni nominali.
  • Attivazione Corretta: Le funzioni barriera trasferite sono diventate attive (avvicinandosi a zero) esattamente quando il drone si avvicinava agli ostacoli, confermando che il trasferimento ha correttamente identificato le situazioni critiche per il sistema fisico completo.

5. Significato e Impatto

Questo lavoro colma un divario critico nella verifica composizionale della sicurezza:

• Generalità: Il metodo non richiede che i due sistemi abbiano la stessa dimensione dello stato o la stessa dinamica, rendendolo applicabile a una vasta gamma di piattaforme robotiche.
• Efficienza Computazionale: Permette di eseguire la sintesi complessa della sicurezza offline su modelli semplificati, riducendo il carico computazionale durante il deployment su sistemi con risorse limitate.
• Futuro: Gli autori indicano come direzione futura l'apprendimento (learning) delle funzioni di simulazione e delle interfacce di controllo dai dati, per estendere l'applicabilità del metodo a sistemi dove i modelli analitici precisi sono difficili da derivare.

In sintesi, il paper dimostra che è possibile garantire la sicurezza formale su sistemi fisici complessi ereditando le garanzie da modelli astratti, purché si introduca un margine di sicurezza calcolato rigorosamente per compensare le differenze dinamiche.