Zero-Shot Signal Temporal Logic Planning with Disjunctive Branch Selection in Dynamic Semantic Maps

Sintesi Tecnica: Pianificazione Zero-Shot in Logica Temporale dei Segnali con Selezione di Rami Disgiuntivi in Mappe Semantiche Dinamiche

1. Formulazione del Problema

Il documento affronta la sfida della pianificazione in Logica Temporale dei Segnali (STL) in ambienti a mappa variabile dove la dinamica del sistema è sconosciuta. L'obiettivo è sintetizzare una traiettoria a orizzonte finito $x_{0:T}$ che soddisfi una specifica STL complessa $\phi$, rispettando al contempo i vincoli di evitamento delle collisioni definiti da una mappa labirintica binaria dinamica $M$.

I vincoli e le sfide chiave includono:

• Generalizzazione Zero-Shot: Il risolutore deve gestire layout di mappa non visti, configurazioni di ostacoli e specifiche STL senza riaddestramento o affinamento specifici per istanza.
• Dinamiche Sconosciute: Il pianificatore opera senza una funzione di transizione esplicita $f(x_t, u_t)$, affidandosi invece a un dataset offline di traiettorie storiche.
• Complessità Disgiuntiva: Le specifiche STL contengono spesso disgiunzioni (operatori OR, $\lor$). La risoluzione di queste richiede la selezione di un ramo specifico della logica da soddisfare. In ambienti dinamici, una selezione non guidata può portare alla scelta di rami geometricamente non fattibili o dinamicamente difficili, causando il fallimento della pianificazione.
• Ancoraggio Temporale: La decomposizione di una formula STL di alto livello in sottocompiti richiede un'allocazione temporale accurata (determinare quando visitare regioni specifiche), il che è difficile da apprendere in modo coerente attraverso geometrie di mappa variabili.

2. Metodologia

Il framework proposto segue un paradigma "decomponi-poi-sintetizza", integrando tre componenti fondamentali:

A. Selezione Euristiche di Rami Disgiuntivi
Per affrontare l'esplosione combinatoria e le questioni di fattibilità delle disgiunzioni, la formula STL viene prima convertita in Forma Normale Disgiuntiva (DNF). Un'euristica leggera classifica quindi i rami candidati ($\phi_k$) per selezionare quello più fattibile ($\phi^*$) basandosi su tre criteri:

1. Complessità degli Operatori Temporali: Penalizza i rami con un annidamento complesso di operatori temporali (es. $U$, $G$), che sono empiricamente più difficili da soddisfare.
2. Raggiungibilità della Mappa: Calcola distanze basate su grafi (es. BFS/DFS) sulla mappa corrente $M$ per penalizzare i rami che richiedono regioni difficili da raggiungere o separate da ostacoli.
3. Flessibilità Temporale: Premia i rami con intervalli di tempo più ampi tra i sottocompiti, offrendo maggiore flessibilità per la generazione della traiettoria.
   Il ramo con il punteggio euristico minimo viene selezionato per la pianificazione a valle.

B. Apprendimento per Rinforzo Transitivo (TRL) per la Previsione del Tempo
Un predittore di tempo appreso stima il numero di passi temporali discreti necessari per viaggiare tra i punti di passaggio degli obiettivi intermedi. Per garantire coerenza temporale attraverso diverse scale e layout di mappa, il predittore viene addestrato utilizzando Apprendimento per Rinforzo Transitivo (TRL) anziché la regressione puntuale standard.

• Meccanismo: Il TRL impone che le lunghezze dei passi previste preservino l'ordinamento relativo implicato dai dati di addestramento. Se la traiettoria $i$ richiede più tempo della traiettoria $j$ nella verità fondamentale, il modello deve prevedere $\hat{\Delta t}_i > \hat{\Delta t}_j$.
• Funzione di Perdita: L'obiettivo di addestramento combina una perdita di regressione $L_1$ con una perdita di ordinamento basata sul margine ($L_{TRL}$) che penalizza le violazioni dei vincoli di ordinamento transitivo. Ciò migliora la calibrazione globale delle stime temporali.

C. Generatore di Traiettorie Transformer Condizionato alla Mappa
La traiettoria finale viene sintetizzata utilizzando un Transformer autoregressivo che si condiziona su:

• Token Mappa: Mappa labirintica binaria codificata $M$ e descrittori di regione.
• Token Tempo: Intervalli temporali derivati dal ramo STL selezionato.
• Prefisso di Traiettoria: La cronologia dello stato corrente.
  Il modello genera la traiettoria token per token (stato per stato). Per mitigare il bias di esposizione durante l'addestramento, viene utilizzato il campionamento programmato, transitando gradualmente dal teacher forcing (utilizzo di stati di verità fondamentale) alla generazione autoregressiva (utilizzo delle previsioni del modello). Il generatore è agnostico rispetto alla dinamica, il che significa che non riceve parametri espliciti del modello dinamico al momento dell'inferenza.

3. Contributi Chiave

1. Gestione Euristiche delle Disgiunzioni: Introduzione di un'euristica leggera a tre criteri per la selezione dei rami disgiuntivi, ampliando significativamente la gamma di specifiche STL risolvibili nella pratica evitando percorsi logici non fattibili.
2. Pianificazione Zero-Shot su Mappe Variabili: Sviluppo di un generatore di traiettorie Transformer condizionato alla mappa che si generalizza a layout di ostacoli e dimensioni di mappa non visti senza riaddestramento, migliorando l'universalità della risoluzione STL.
3. Apprendimento per Rinforzo Transitivo per l'Ancoraggio Temporale: Applicazione del TRL per addestrare il predittore di tempo, garantendo un'allocazione temporale coerente tra i sottocompiti decomposti e migliorando la robustezza complessiva della soddisfazione STL.
4. Validazione Empirica: Dimostrazione di guadagni coerenti nelle prestazioni attraverso ambienti diversi (complessità di mappa variabile) e dinamiche (modelli a doppio integratore e unicycle), validando la robustezza del framework rispetto agli spostamenti di distribuzione.

4. Risultati Sperimentali

Gli esperimenti sono stati condotti su un benchmark di navigazione basato su griglia (famiglia U-Maze) con dimensioni di mappa di $5\times5$, $7\times7$ e $9\times9$, sia sotto dinamiche a doppio integratore (DI) che unicycle (UNI).

• Tasso di Successo: Il metodo proposto ha ottenuto miglioramenti coerenti nei tassi di successo rispetto a una baseline (lo stesso metodo senza selezione euristica dei rami). I guadagni sono stati più pronunciati in mappe più grandi e complesse (es. $9\times9$), dove l'euristica ha efficacemente potato i rami non fattibili.
• Robustezza: I valori di robustezza (misura quantitativa della soddisfazione STL) sono rimasti comparabili o superiori alla baseline, indicando che tassi di successo più elevati non sono stati ottenuti sacrificando i margini delle specifiche.
• Efficienza: Sebbene il tempo di pianificazione nominale fosse comparabile alla baseline, l'inclusione della selezione euristica ha sostanzialmente ridotto il tempo di pianificazione effettivo potando lo spazio di ricerca in anticipo.
• Generalizzazione: Il generatore di traiettorie ha sintetizzato con successo traiettorie fattibili sia per le dinamiche DI che UNI senza input espliciti del modello dinamico, dimostrando una forte trasferibilità tra modelli di movimento.

5. Significato e Affermazioni

Il documento afferma che il suo significato primario risiede nel colmare il divario tra ragionamento logico formale e sintesi di traiettorie basata sui dati in ambienti dinamici e sconosciuti. Disaccoppiando la ramificazione logica di alto livello (tramite l'euristica) dalla realizzazione geometrica di basso livello (tramite il Transformer), il framework affronta la fragilità dei pianificatori zero-shot esistenti di fronte a geometrie di mappa variabili e logica disgiuntiva complessa.

Gli autori sottolineano che il loro approccio offre una soluzione scalabile e zero-shot che non richiede riaddestramento specifico per l'ambiente, rendendolo una direzione promettente per il dispiegamento di pianificatori basati su STL in scenari reali dove mappe e ostacoli cambiano in modo imprevedibile. L'integrazione del TRL è evidenziata come un metodo innovativo per migliorare la coerenza temporale dei pianificatori appresi, un fattore critico per soddisfare vincoli temporali a lungo orizzonte.