Robustness-Based Synthesis for Time Window Temporal Logic Specifications via Mixed-Integer Linear Programming

Sintesi Tecnica: Sintesi Basata sulla Robustezza per Specifiche di Logica Temporale a Finestra Temporale tramite Programmazione Lineare Intera Mista

Definizione del Problema
Il documento affronta il problema della sintesi del controllo per sistemi lineari a tempo discreto soggetti a specifiche di Logica Temporale a Finestra Temporale (TWTL). La TWTL è un linguaggio di specifica progettato per i sistemi cyber-fisici che esprime in modo compatto compiti sequenziali con vincoli temporali espliciti (ad esempio, "rimanere nella regione A per 4 unità, poi visitare la regione B entro 10 unità"). Mentre lavori precedenti hanno stabilito la TWTL per il monitoraggio e la pianificazione basata sul campionamento, mancava una procedura di sintesi deterministica che ottimizzasse la robustezza — una misura quantitativa di quanto bene una traiettoria soddisfi una specifica — ovvero la resilienza della soddisfazione. Gli autori mirano a sintetizzare input di controllo che non solo soddisfino la formula booleana TWTL, ma che massimizzino anche il margine di soddisfazione (robustezza), aumentando la resilienza a disturbi e rumore.

Metodologia
La metodologia proposta codifica la semantica quantitativa (robustezza) della TWTL in un Programma Lineare Intero Misto (MILP).

1. Codifica della Robustezza: Basandosi sulla semantica quantitativa introdotta in un lavoro precedente [1], gli autori definiscono un valore di robustezza $\rho$ per le formule TWTL. Essi traducono la definizione ricorsiva di $\rho$ (che coinvolge operazioni min/max su finestre temporali) in un insieme di vincoli lineari utilizzando formulazioni "Big-M" e variabili binarie.

   • Operatori: La codifica gestisce gli operatori specifici della TWTL: Hold ($H_d$), Within ($[\cdot]_{[a,b]}$) e Concatenation ($\cdot$).
   • Variabili Binarie: Le operazioni logiche (disgiunzione, within, concatenazione) sono codificate utilizzando variabili binarie. Gli autori osservano che il numero di variabili binarie è una metrica critica delle prestazioni.

2. Formulazioni di Sintesi: Vengono formulate due problemi di sintesi:

   • Open-Loop: Un'ottimizzazione singola dallo stato iniziale $x_0$ per trovare una sequenza di controllo $u^*$ che massimizzi $\rho$.
   • Closed-Loop (MPC): Un framework di Controllo Predittivo del Modello (MPC) che risolve nuovamente il MILP ad ogni passo temporale $t$ utilizzando lo stato misurato corrente $x_t$ e lo stato corrente dell'Automa a Stati Finiti Deterministico (DFA) della TWTL.

3. Orizzonte Adattivo al Task & Warm-Start: Un'innovazione chiave nella formulazione MPC è l'orizzonte adattivo al task.

   • Inveve di utilizzare l'intero orizzonte della formula $T$ (che può essere grande) per ogni risoluzione, l'orizzonte $H_t$ è limitato dinamicamente alla finestra temporale rimanente del sotto-task attivo corrente identificato dallo stato del DFA.
   • Gli autori utilizzano una strategia di warm-start. Poiché le matrici dei vincoli del MILP dipendono dallo stato del DFA (che è finito e indipendente dai limiti temporali) piuttosto che dai valori di stato specifici, essi precomputano le matrici per ogni stato del DFA offline. Online, aggiornano solo il termine noto (valori di stato) e i limiti, riducendo significativamente l'overhead computazionale.

Contributi Principali
Il documento presenta quattro contributi primari:

1. Codifica MILP: Fornisce la prima codifica MILP Big-M ricorsiva per la robustezza TWTL, dimostrando che qualsiasi soluzione ammissibile con un valore obiettivo positivo garantisce la soddisfazione booleana della specifica (Teorema 4.1).
2. Framework di Sintesi: Formula sia un controllore open-loop che un controllore MPC closed-loop. La formulazione MPC introduce un orizzonte adattivo al task che sfrutta la struttura del DFA della TWTL per limitare l'orizzonte di predizione alla finestra rimanente del task corrente ($\max b_i$) anziché all'orizzonte totale della formula $T$.
3. Strategia di Efficienza: Propone una strategia di warm-start che riduce il costo online per passo del MPC a una complessità lineare rispetto alla dimensione dello stato del sistema ($O(n)$) per gli aggiornamenti, più il costo di risoluzione di un MILP progressivamente più piccolo.
4. Efficienza Comparativa: Dimostra che la codifica diretta TWTL è più efficiente rispetto alla traduzione della TWTL in STL per la sintesi MILP, in particolare all'aumentare del numero di sotto-task sequenziali.

Risultati
Gli autori validano il loro approccio attraverso esperimenti numerici su un sistema double-integrator 2D che naviga in uno spazio di lavoro con ostacoli e visite a regioni sequenziali.

• Rilevanza della Robustezza: I confronti mostrano che i percorsi ottimizzati per la robustezza sono qualitativamente e quantitativamente più resilienti ai disturbi rispetto a quelli che soddisfano solo i vincoli booleani.
• Open-Loop vs. Closed-Loop: In presenza di disturbi, il controllore open-loop fallisce nel completare il compito, mentre il controllore MPC closed-loop si adatta e riprogramma con successo.
• Confronto delle Prestazioni:
  • TWTL vs. STL: Per specifiche con quattro o più sotto-task, la codifica diretta TWTL supera la traduzione STL in termini di tempo di risoluzione grazie a una riduzione delle variabili binarie.
  • Strategie di Orizzonte: La strategia dell'orizzonte "Task-Adaptive" (basata su DFA) riduce significativamente il tempo totale di risoluzione durante un'esecuzione rispetto a un approccio a orizzonte fisso (analogo ai precedenti lavori MPC su STL), con un divario di prestazioni che si amplia all'aumentare del numero di obiettivi sequenziali.

Significatività e Rivendicazioni
Il documento sostiene di fornire la prima procedura di sintesi MILP per la massimizzazione della robustezza per la TWTL. La sua significatività risiede nel colmare il divario tra le specifiche di logica temporale di alto livello e l'esecuzione del controllo robusto in tempo reale.

• Garanzie Deterministiche: A differenza dei pianificatori basati sul campionamento che offrono completezza probabilistica, questo approccio offre garanzie deterministiche sulla massimizzazione della robustezza.
• Scalabilità: Sfruttando la struttura DFA della TWTL, il metodo evita l'esplosione computazionale associata ai grandi orizzonti temporali nelle formulazioni MPC tradizionali, rendendolo adatto a compiti sequenziali complessi.
• Praticità: La strategia di warm-start e l'orizzonte adattivo al task rendono l'approccio computazionalmente trattabile per l'implementazione online, affrontando la "maledizione della dimensionalità" spesso associata al controllo basato su logica temporale tramite MILP.

Gli autori concludono che, sebbene l'attuale lavoro si concentri sulla misura di robustezza min-max, il lavoro futuro esplorerà l'estensione di questa alla robustezza Arithmetic Geometric Mean (AGM) e l'utilizzo della riscrittura delle formule per ridurre ulteriormente il conteggio delle variabili binarie.