Neural Vector Lyapunov-Razumikhin Certificates for Delayed Interconnected Systems

1. Il Problema

Il lavoro affronta la sfida critica di garantire la stabilità scalabile input-to-state (sISS) per sistemi interconnessi su larga scala (come flotte di veicoli autonomi, formazioni di droni e microreti elettriche) in presenza di ritardi di comunicazione.

• Contesto: I sistemi interconnessi moderni sono complessi e accoppiati. I ritardi introdotti da sensori, calcolo e trasmissione di rete degradano spesso le prestazioni e minacciano la stabilità.
• Limiti degli approcci esistenti:
  • I metodi basati su modelli (es. controllo predittivo) richiedono modelli dinamici accurati, che sono spesso difficili da ottenere o incerti.
  • I metodi basati sull'apprendimento (es. reti neurali) offrono buone prestazioni empiriche ma sono "scatole nere", rendendo difficile fornire garanzie formali di stabilità, specialmente per sistemi con ritardi.
  • Le certificazioni esistenti per sistemi ritardati non sono scalabili (la complessità cresce esponenzialmente con il numero di agenti) o richiedono ipotesi restrittive (es. sistemi a valori positivi).

L'obiettivo è sviluppare un framework che sintetizzi e verifichi certificati di stabilità formali per sistemi interconnessi discreti, ritardati e su larga scala, senza assumere la conoscenza esplicita delle dinamiche locali.

2. Metodologia

Gli autori propongono un framework che combina teoria del controllo, apprendimento automatico e verifica formale.

A. Fondamenti Teorici: Funzioni di Lyapunov-Razumikhin Vettoriali

Il cuore teorico è l'istituzione di una condizione sufficiente per la sISS discreta basata su funzioni di Lyapunov-Razumikhin vettoriali.

• Invece di una singola funzione di Lyapunov, si utilizza una famiglia di funzioni locali $\{V_i\}$, una per ogni agente.
• Viene introdotta una condizione condizionale di tipo Razumikhin: se i valori delle funzioni di Lyapunov degli stati passati (ritardati) sono sufficientemente piccoli rispetto allo stato corrente, allora la funzione di Lyapunov attuale deve decrescere.
• Viene definito un vincolo di small-gain (guadagno piccolo) sui coefficienti di accoppiamento $\gamma_{i,j}$ che garantisce la contrazione del sistema indipendentemente dalla dimensione della rete $N$.

B. Sintesi e Verifica con Reti Neurali

Poiché le funzioni $V_i$ sono difficili da progettare manualmente, il framework le apprende tramite reti neurali:

1. Sintesi: Si addestra una rete neurale per approssimare le funzioni di Lyapunov e una matrice di accoppiamento $\Gamma$ che soddisfi le condizioni del teorema. La funzione di perdita include termini per i limiti di classe-K$\infty$, la condizione di decremento condizionale e la vicinanza a una politica nominale.
2. Verifica su Domini Vincolati dalla Raggiungibilità: Verificare l'intera spazio degli stati è intrattabile. Il metodo restringe la verifica ai domini di ritardo che sono raggiungibili da un insieme di stati iniziali entro un orizzonte finito.
3. Strategia a Due Stadi:
   • Fase Esterna: Si verifica la logica condizionale di Razumikhin per gli stati fuori da una regione di interesse (livello superiore).
   • Fase Interna: Si verifica una contrazione incondizionata all'interno di una regione di livello definita ($V_{max} \le R$).
4. Verifica Basata sul Campionamento: Sfruttando la continuità di Lipschitz delle dinamiche e delle funzioni neurali, il problema di verifica continuo viene ridotto a un numero finito di controlli su una griglia campionata, con margini di sicurezza deterministici.

C. Scalabilità e Riutilizzo dei Certificati

Per gestire sistemi su larga scala, il framework introduce due concetti chiave:

• Isomorfismo di Sottosezione: Se un sistema grande contiene sottosezioni strutturalmente equivalenti a un sistema più piccolo, il certificato appreso per il sistema piccolo può essere riutilizzato per il grande.
• Equivalenza Strutturale dei Nodi: Nodi con dinamiche, topologie di connessione e ritardi identici possono condividere lo stesso certificato neurale, riducendo drasticamente la complessità computazionale.

3. Contributi Chiave

1. Condizione Teorica: Dimostrazione di una condizione sufficiente per la sISS discreta in sistemi interconnessi ritardati usando funzioni vettoriali di Lyapunov-Razumikhin, permettendo certificazioni indipendenti dalla scala.
2. Pipeline di Sintesi e Verifica Scalabile: Sviluppo di un framework che apprende certificati neurali e li verifica su domini di ritardo vincolati dalla raggiungibilità, con analisi di complessità che dimostra come la verifica possa essere riutilizzata per sistemi strutturalmente equivalenti.
3. Validazione Empirica: Applicazione e validazione su tre scenari reali complessi:
   • Flotte di veicoli a guida autonoma mista (mixed-autonomy platoons).
   • Formazioni di droni (UAV).
   • Microreti elettriche (inverter).

4. Risultati Sperimentali

I risultati sono stati confrontati con diverse baseline (controllore nominale, feedback predittivo, certificati ISS composti, sISS senza ritardi).

• Efficienza di Verifica:
  • Il metodo proposto è l'unico in grado di completare la verifica in tempi ragionevoli per sistemi su larga scala (es. 50 agenti).
  • Le varianti che usano solo la riduzione della raggiungibilità o solo la riutilizzabilità strutturale falliscono o richiedono tempi di esecuzione eccessivi (timeout).
  • Il tempo di verifica rimane quasi costante all'aumentare del numero di agenti $N$, dimostrando la scalabilità.
• Prestazioni di Controllo:
  • In tutti e tre gli scenari, il metodo proposto ha ottenuto i minori errori quadratici medi (RMSE) rispetto alle baseline, sia in presenza di disturbi sinusoidali che di disturbi iniziali.
  • Ad esempio, nella flotta di veicoli, ha ridotto l'RMSE del 22,86% rispetto al controllo nominale e ha superato il feedback predittivo (che richiede un modello preciso) senza utilizzare un modello esplicito.
• Visualizzazione: Le simulazioni mostrano che le funzioni di Lyapunov neurali crescono con la deviazione dallo stato di equilibrio e che le traiettorie del sistema convergono o rimangono limitate attorno ai valori desiderati.

5. Significato e Impatto

Questo lavoro colma un divario significativo tra l'apprendimento automatico e la teoria del controllo formale per sistemi complessi.

• Sicurezza Formale: Fornisce garanzie matematiche rigorose di stabilità per controllori basati su reti neurali in ambienti con ritardi, un requisito fondamentale per applicazioni critiche come i trasporti e le reti energetiche.
• Scalabilità: Risolve il problema della "maledizione della dimensionalità" nella verifica di sistemi interconnessi, permettendo di scalare la certificazione a reti molto grandi sfruttando la struttura del sistema.
• Applicabilità: Il framework è agnostico rispetto al modello dinamico specifico, rendendolo adatto a sistemi reali dove le dinamiche esatte sono sconosciute o difficili da modellare.

In sintesi, il paper presenta un passo avanti fondamentale verso l'adozione sicura e affidabile di sistemi di controllo basati sull'IA in infrastrutture critiche soggette a ritardi di comunicazione.