Value Functions for Temporal Logic: Optimal Policies and Safety Filters

Riepilogo Tecnico: Funzioni di Valore per la Logica Temporale: Politiche Ottimali e Filtri di Sicurezza

Enunciato del Problema
Mentre le equazioni di Bellman per i problemi fondamentali di raggiungimento, evitamento e raggiungimento-evitamento sono ben consolidate, la relazione tra ottimalità del valore e ottimalità della politica diventa sottile in contesti di orizzonte infinito non scontati, in particolare per specifiche complesse di Logica Temporale (TL). Sorge una patologia critica in cui la massimizzazione avida della funzione Q può produrre politiche che rimandano indefinitamente il completamento del compito per problemi di raggiungimento-evitamento (equivalenti a specifiche Until), anche quando la funzione di valore è essa stessa ottimale. Ciò avviene perché la sequenza di azioni ottimale per traiettorie infinite è fondamentalmente non markoviana; l'input ottimale potrebbe dover "passare" dalla massimizzazione del valore corrente a un valore costitutivo in un grafo di decomposizione per soddisfare le specifiche rimanenti di orizzonte infinito. I metodi esistenti, come l'aumento dello stato per problemi a doppio obiettivo, faticano a generalizzarsi a formule complesse che coinvolgono specifiche Until, Globally e Globally-Until nidificate. Inoltre, vi è la necessità di filtri di sicurezza che garantiscano la soddisfazione di specifiche TL complesse, andando oltre i semplici compiti di evitamento o di raggiungimento-evitamento.

Metodologia
Gli autori propongono un quadro che generalizza le funzioni di valore e Q agli storia degli stati per gestire la natura non markoviana del problema. La metodologia si basa sulla decomposizione algebrica della funzione di valore per la TL in un grafo di funzioni di valore costitutive.

1. Funzioni di Valore Non Markoviane: Il documento definisce le funzioni di valore ottimali $V^*$ e le funzioni Q su storie di stati $x_{0:t}$ piuttosto che sui soli stati correnti. Ciò permette alla politica di tenere conto della storia necessaria per soddisfare i vincoli temporali.
2. Sistemi con Tempo Augmentato e Tempi di Testimone: Per affrontare il problema del rinvio nelle specifiche Until ($U$), gli autori introducono un sistema con tempo aumentato dotato di un timer. Definiscono un "tempo di testimone ottimale" $\sigma^*$, che è il momento più presto in cui una traiettoria raggiunge il punteggio di robustezza ottimale. Ciò consente la costruzione di politiche che passano da una strategia avida a orizzonte finito (massimizzando la funzione Q entro il tempo di testimone) a una politica di suffisso che soddisfa la sotto-formula rimanente.
3. Costruzione Compositiva delle Politiche: Il documento costruisce politiche ottimali per un frammento specifico di formule TL (Definizione 3), che include:
   • Formule proposizionali.
   • Operatori Until ($p U \phi$), Next ($X\phi$) e Globally ($Gp$).
   • Globally-Until ($G(\bigvee p_i U r_i)$), che codifica i criteri di accettazione di Büchi.
   • Disgiunzioni e congiunzioni proposizionali.
     La costruzione assume l'esistenza di politiche ottimali per le sotto-formule (Assunzione 2) e le combina ricorsivamente. Per Globally-Until, la politica visita iterativamente ogni componente Until in sequenza per garantire visite infinite agli insiemi di stati richiesti.
4. Filtraggio di Sicurezza: Gli autori dimostrano che la funzione Q può servire come filtro di sicurezza. Definiscono un insieme di fallimento in cui la specifica non può essere soddisfatta con una robustezza non negativa. Viene proposto uno schema di intervento il meno restrittivo possibile: se l'azione di una politica nominale produce un valore Q non negativo (indicando la soddisfacibilità futura), essa è consentita; altrimenti, il sistema passa all'azione che massimizza la funzione Q. Sotto specifiche assunzioni (ad esempio, assenza di operatori Until illimitati), questo filtro garantisce la soddisfazione della specifica.

Contributi Chiave

1. Generalizzazione delle Funzioni di Valore: Il documento generalizza la funzione di valore ottimale e la funzione Q alle storie di stati (Definizione 1) e definisce l'ottimalità sulle storie (Definizione 2), affrontando la natura non markoviana dei problemi TL a orizzonte infinito.
2. Politiche Ottimali Compositive: Per una vasta classe di formule TL (Definizione 3), gli autori costruiscono politiche ottimali compositive per la metrica di robustezza associata (Teoremi 1–8). Ciò include la gestione della patologia del rinvio nelle specifiche Until e Globally-Until.
3. Filtri di Sicurezza il Meno Restrittivi Possibile: Il lavoro dimostra che la funzione Q su storie (potenzialmente sub-ottimali) produce un filtro di sicurezza il meno restrittivo possibile per una politica nominale (Teoremi 9, 10). Questo filtro garantisce la soddisfazione della specifica rispettando il percorso precedente della politica nominale, a condizione che la formula soddisfi determinati vincoli strutturali.

Risultati e Dimostrazioni
Il documento convalida il quadro proposto attraverso dimostrazioni teoriche e due dimostrazioni hardware/software:

• GridWorld a Due Agenti: Gli autori risolvono un problema congiunto di stato-azione a 4 dimensioni con una specifica complessa che coinvolge vincoli di raggiungimento, sicurezza e vivacità limitati nel tempo. Dimostrano che la politica ottimale derivata ($\pi_{spec}$) guida con successo il sistema a soddisfare la specifica. Inoltre, quando utilizzata come filtro per politiche nominali di "caffè" e "tè" (che singolarmente non riescono a soddisfare la specifica congiunta), il filtro garantisce che il sistema congiunto soddisfi il compito complesso, mentre un filtro standard "solo sicurezza" porta a deadlock e fallimento.
• Drona Singolo Agente: Utilizzando un drone Crazyflie, gli autori dimostrano la politica in un compito di navigazione con ostacoli. Il filtro TL proposto guida con successo il drone verso un cantiere rispettando vincoli temporali complessi (ad esempio, looping attraverso zone specifiche, evitando muri). Al contrario, una politica nominale non filtrata o un filtro basato solo su vincoli di sicurezza porta il drone a rimanere intrappolato o a schiantarsi.

Significato
Il documento afferma di offrire un approccio pratico per generare politiche ottimali per il valore di una vasta classe di formule TL estendendo i recenti risultati di decomposizione. Il suo significato principale risiede nella risoluzione della patologia in cui la massimizzazione avida di Q fallisce per compiti a orizzonte infinito e nel fornire un meccanismo per sintetizzare filtri di sicurezza che garantiscano la soddisfazione di compiti complessi, non solo della sicurezza. Estendendo la portata delle formule risolvibili per includere specifiche Until e Globally-Until nidificate, il lavoro colma il divario tra la raggiungibilità di Hamilton-Jacobi e l'Apprendimento per Rinforzo per compiti temporali complessi e critici per la sicurezza.