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

Resumo Técnico: Planejamento de Lógica Temporal de Sinal Zero-Shot com Seleção de Ramificação Disjuntiva em Mapas Semânticos Dinâmicos

1. Formulação do Problema

O artigo aborda o desafio do planejamento de Lógica Temporal de Sinal (STL) em ambientes de mapas variáveis onde a dinâmica do sistema é desconhecida. O objetivo é sintetizar uma trajetória de horizonte finito $x_{0:T}$ que satisfaça uma especificação STL complexa $\phi$, ao mesmo tempo em que adere a restrições de evitar colisões definidas por um mapa de labirinto binário dinâmico $M$.

As principais restrições e desafios incluem:

• Generalização Zero-Shot: O solucionador deve lidar com layouts de mapas não vistos, configurações de obstáculos e especificações STL sem re-treinamento ou ajuste fino específicos para cada instância.
• Dinâmica Desconhecida: O planejador opera sem uma função de transição explícita $f(x_t, u_t)$, confiando, em vez disso, em um conjunto de dados offline de trajetórias históricas.
• Complexidade Disjuntiva: Especificações STL frequentemente contêm disjunções (operadores OU, $\lor$). Resolver essas disjunções exige selecionar um ramo específico da lógica para satisfazer. Em ambientes dinâmicos, a seleção não orientada pode levar à escolha de ramos que são geometricamente inviáveis ou dinamicamente difíceis, causando falha no planejamento.
• Ancoragem Temporal: Decompor uma fórmula STL de alto nível em subtarefas requer alocação temporal precisa (determinar quando visitar regiões específicas), o que é difícil de aprender consistentemente através de geometrias de mapas variáveis.

2. Metodologia

O framework proposto segue um paradigma de "decompor-então-sintetizar", integrando três componentes principais:

A. Seleção Heurística de Ramificação Disjuntiva
Para abordar a explosão combinatória e os problemas de viabilidade das disjunções, a fórmula STL é primeiro convertida para a Forma Normal Disjuntiva (DNF). Uma heurística leve então classifica os ramos candidatos ($\phi_k$) para selecionar o mais viável ($\phi^*$) com base em três critérios:

1. Complexidade de Operadores Temporais: Penaliza ramos com aninhamento complexo de operadores temporais (por exemplo, $U$, $G$), que empiricamente são mais difíceis de satisfazer.
2. Acessibilidade do Mapa: Calcula distâncias baseadas em grafos (por exemplo, BFS/DFS) no mapa atual $M$ para penalizar ramos que exigem regiões difíceis de alcançar ou separadas por obstáculos.
3. Folga Temporal: Recompensa ramos com maiores intervalos de tempo entre subtarefas, oferecendo mais flexibilidade para a geração de trajetórias.
   O ramo com a pontuação heurística mínima é selecionado para o planejamento a jusante.

B. Aprendizado por Reforço Transitivo (TRL) para Previsão de Tempo
Um preditor de tempo aprendido estima o número de passos de tempo discretos necessários para viajar entre waypoints de sub-objetivos. Para garantir consistência temporal através de diferentes escalas e layouts de mapas, o preditor é treinado usando Aprendizado por Reforço Transitivo (TRL) em vez de regressão pontual padrão.

• Mecanismo: O TRL impõe que os comprimentos de passo previstos preservem a ordenação relativa implicada pelos dados de treinamento. Se a trajetória $i$ leva mais tempo que a trajetória $j$ na verdade fundamental, o modelo deve prever $\hat{\Delta t}_i > \hat{\Delta t}_j$.
• Função de Perda: O objetivo de treinamento combina uma perda de regressão $L_1$ com uma perda de classificação baseada em margem ($L_{TRL}$) que penaliza violações das restrições de ordenação transitiva. Isso melhora a calibração global das estimativas de tempo.

C. Gerador de Trajetória Transformer Condicionado ao Mapa
A trajetória final é sintetizada usando um Transformer autoregressivo que condiciona em:

• Tokens de Mapa: Mapa de labirinto binário codificado $M$ e descritores de região.
• Tokens de Tempo: Intervalos temporais derivados do ramo STL selecionado.
• Prefixo de Trajetória: O histórico do estado atual.
  O modelo gera a trajetória token por token (estado por estado). Para mitigar o viés de exposição durante o treinamento, é empregada amostragem agendada, transitando gradualmente do ensino forçado (usando estados de verdade fundamental) para geração autoregressiva (usando previsões do modelo). O gerador é agnóstico à dinâmica, o que significa que não recebe parâmetros explícitos do modelo dinâmico no momento da inferência.

3. Principais Contribuições

1. Tratamento Heurístico de Disjunções: Introdução de uma heurística leve de três critérios para selecionar ramos disjuntivos, expandindo significativamente a gama de especificações STL solucionáveis na prática ao evitar caminhos lógicos inviáveis.
2. Planejamento Zero-Shot em Mapas Variáveis: Desenvolvimento de um gerador de trajetória Transformer condicionado ao mapa que generaliza para layouts de obstáculos não vistos e tamanhos de mapa sem re-treinamento, aprimorando a universalidade da resolução STL.
3. Aprendizado por Reforço Transitivo para Ancoragem Temporal: Aplicação de TRL para treinar o preditor de tempo, garantindo alocação temporal consistente através de subtarefas decompostas e melhorando a robustez geral da satisfação STL.
4. Validação Empírica: Demonstração de ganhos consistentes de desempenho através de ambientes diversos (variando complexidades de mapas) e dinâmicas (modelos de duplo integrador e unicycle), validando a robustez do framework a deslocamentos de distribuição.

4. Resultados Experimentais

Os experimentos foram conduzidos em um benchmark de navegação baseado em grade (família U-Maze) com tamanhos de mapa de $5\times5$, $7\times7$ e $9\times9$, sob dinâmicas de duplo integrador (DI) e unicycle (UNI).

• Taxa de Sucesso: O método proposto alcançou melhorias consistentes nas taxas de sucesso em comparação com uma linha de base (o mesmo método sem seleção heurística de ramos). Os ganhos foram mais pronunciados em mapas maiores e mais complexos (por exemplo, $9\times9$), onde a heurística podou efetivamente ramos inviáveis.
• Robustez: Os valores de robustez (medida quantitativa da satisfação STL) permaneceram comparáveis ou superaram a linha de base, indicando que taxas de sucesso mais altas não foram alcançadas sacrificando as margens da especificação.
• Eficiência: Embora o tempo de planejamento nominal fosse comparável à linha de base, a inclusão da seleção heurística reduziu substancialmente o tempo de planejamento efetivo ao podar o espaço de busca precocemente.
• Generalização: O gerador de trajetória sintetizou com sucesso trajetórias viáveis para ambas as dinâmicas DI e UNI sem entradas explícitas de modelo dinâmico, demonstrando forte transferibilidade entre modelos de movimento.

5. Significado e Alegações

O artigo afirma que seu principal significado reside em preencher a lacuna entre raciocínio lógico formal e síntese de trajetória orientada por dados em ambientes dinâmicos e desconhecidos. Ao desacoplar o ramificação lógica de alto nível (via heurística) da realização geométrica de baixo nível (via Transformer), o framework aborda a fragilidade dos planejadores zero-shot existentes ao enfrentar geometrias de mapas variáveis e lógica disjuntiva complexa.

Os autores enfatizam que sua abordagem oferece uma solução escalável e zero-shot que não requer re-treinamento específico do ambiente, tornando-se uma direção promissora para implantar planejadores baseados em STL em cenários do mundo real onde mapas e obstáculos mudam de forma imprevisível. A integração do TRL é destacada como um método inovador para melhorar a coerência temporal de planejadores aprendidos, um fator crítico para satisfazer restrições temporais de longo horizonte.