TERA: A Unified Taylor Model Enabled Reachability Analysis Framework

Sintesi Tecnica: TERA – Un Framework di Analisi di Raggiungibilità basato su Modelli di Taylor Unificati

Definizione del Problema
La verifica di sistemi critici per la sicurezza, definiti da dinamiche del tipo $\dot{x} = f(x, u, w)$ dove $w$ rappresenta disturbi limitati o incertezze, richiede l'approssimazione rigorosa di tutti i possibili inviluppi delle traiettorie di stato su un orizzonte temporale finito. Sebbene il calcolo esatto dei flowpipe sia generalmente impraticabile per sistemi non lineari, sono necessarie sovra-approssimazioni basate su insiemi. Tuttavia, le rappresentazioni tradizionali come gli (iper-)intervalli e i zonotopi soffrono dell'effetto "wrapping" (effetto avvolgimento), in cui le sovra-approssimazioni accumulate portano a inviluppi di insiemi raggiungibili eccessivamente conservativi. Inoltre, gli strumenti esistenti basati su Modelli di Taylor (TM) (ad es., Flow*, CORA, JuliaReach) sono spesso scritti in linguaggi compilati (C++, MATLAB, Julia), il che rende difficile la prototipazione rapida, oppure mancano del supporto per sistemi stocastici e classi ampie di sistemi all'interno di un workflow unificato.

Metodologia
TERA affronta queste limitazioni fornendo un framework nativo in Python che si integra con l'ecosistema scientifico di Python e sfrutta il sistema di algebra computazionale SageMath. La metodologia principale si basa sui Modelli di Taylor (TM) della forma $P(x_0, t) + I$, dove $P$ è un'approssimazione polinomiale di Taylor di alto ordine della soluzione e $I$ è un resto intervallare che garantisce l'inclusione della soluzione reale.

I componenti metodologici chiave includono:

• Propagazione: Le dinamiche in tempo continuo sono propagate utilizzando schemi di integrazione TM validati, basati sul lavoro di Berz e Makino, insieme ad approcci di costruzione di flowpipe per sistemi non lineari di Chen.
• Mitigazione dell'Effetto Wrapping: Per mantenere inviluppi stretti su lunghi orizzonti temporali, TERA implementa la propagazione composizionale sinistra-destra utilizzando il metodo di "shrink-wrapping".
• Supporto ai Sistemi:
  • ODE Non Lineari: Supporta sistemi con non linearità non polinomiali (ad es., funzioni trascendenti come $\sin$ e $\cos$).
  • Sistemi Ibridi: Calcola le intersezioni dei guard di automi ibridi e le transizioni discrete seguendo la semantica di raggiungibilità ibrida basata su TM.
  • Sistemi Stocastici: Per i sistemi stocastici in tempo continuo, TERA combina i flowpipe TM deterministici con limiti di deviazione probabilistica per calcolare gli inviluppi di insiemi raggiungibili $\delta$-probabilistici ($\delta$-PRS). Ciò garantisce che le traiettorie rimangano all'interno degli insiemi calcolati con una probabilità di almeno $1-\delta$.
• Aritmetica Rigorosa: L'arrotondamento corretto è ottenuto tramite la libreria GNU MPFR integrata in SageMath per garantire il rigore matematico.

Contributi Chiave

1. Framework Unificato: TERA è presentato come il primo framework gratuito, open-source e nativo in Python capace di gestire sistemi continui, ibridi e stocastici all'interno di un unico workflow simbolico-numerico.
2. Estensibilità: Sfruttando Python e SageMath, il framework facilita la prototipazione rapida di tecniche di analisi di raggiungibilità, affrontando la rigidità degli esistenti strumenti C++ o MATLAB proprietari.
3. Capacità Stocastica: Il framework estende l'analisi di raggiungibilità basata su TM ai sistemi stocastici in tempo continuo, calcolando inviluppi $\delta$-PRS.
4. Disponibilità Aperta: Il software è distribuito sotto licenza GPLv2 ed è disponibile tramite GitHub.

Risultati e Validazione
Gli autori hanno validato TERA rispetto alla suite di problemi benchmark della competizione ARCH [5]. I risultati dimostrano la capacità del framework di calcolare sovra-approssimazioni strette degli insiemi raggiungibili per problemi benchmark difficili:

• Sistemi Continui Non Lineari: TERA ha calcolato con successo un inviluppo stretto per una rete di reazione biochimica di tipo Laub-Loomis a 7 dimensioni su $t \in [0, 20]$ in 13 secondi. Ha inoltre scalato a un problema di quadrotor controllato a 12 dimensioni che coinvolge funzioni trascendenti.
• Sistemi Ibridi: Il framework ha generato inviluppi rigorosi per un sistema ibrido di una pallina che rimbalza (bouncing ball), proiettando correttamente i flowpipe sul piano $(x, t)$ distinguendo tra modalità attive (su/giù).
• Sistemi Stocastici: TERA ha calcolato un inviluppo $\delta$-PRS ($\delta = 0.001$) per un modello a molla stocastico su $t \in [0, 20]$. Si è dimostrato che l'inviluppo risultante conteneva 2000 percorsi campionati tramite Monte Carlo Euler-Maruyama.

Significato e Prospettive Future
Il documento posiziona TERA come un passo fondamentale verso un'infrastruttura Python robusta e open-source per l'analisi di raggiungibilità rigorosa. Il suo significato risiede nella democratizzazione dell'accesso ai metodi basati su TM di alto ordine per una vasta classe di sistemi, inclusi quelli con disturbi stocastici. Gli autori dichiarano che il lavoro in corso è focalizzato sull'estensione delle capacità ai sistemi ibridi stocastici. L'obiettivo a lungo termine è applicare questa infrastruttura ad classi di sistemi ancora più ampie, come quelle controllate da reti neurali artificiali. Gli autori mantengono un tono modesto, osservando che, sebbene l'attuale implementazione gestisca benchmark difficili, il framework è progettato per evolversi al fine di supportare classi di sistemi più complesse.