Infinite Trace Objectives with Finite Trace Techniques: Translating LTL to LTLf+

Resumo Técnico: Objetivos de Traço Infinito com Técnicas de Traço Finito

Problema
A Lógica Temporal Linear (LTL) é a linguagem padrão para especificar objetivos temporais em IA, variodando de síntese reativa a planejamento em processos de decisão de Markov. No entanto, resolver problemas baseados em LTL tradicionalmente requer a tradução de uma fórmula LTL para um autômato não determinístico sobre palavras infinitas e a subsequente determinação deste. Este passo de determinação é notoriamente difícil, tanto teórica quanto praticamente, criando uma barreira significativa à escalabilidade. Enquanto avanços recentes na síntese LTL utilizam uma forma normal (baseada na hierarquia de segurança-progressão de Manna-Pnueli) para decompor fórmulas em componentes determinísticos, a tradução de LTL para autômatos determinísticos permanece duplamente exponencial.

Concomitantemente, a lógica LTLf (LTL sobre traços finitos) ganhou tração devido à sua capacidade de ser traduzida eficientemente para Autômatos Finitos Determinísticos (DFA), que suportam minimização eficiente. A LTLf+ foi introduzida recentemente para elevar a LTLf a traços infinitos, quantificando sobre prefixos, correspondendo às classes da hierarquia de Manna-Pnueli. Embora a L Lf+ possua o mesmo poder expressivo que a LTL, uma tradução construtiva de LTL para LTLf+ era anteriormente inexistente, limitando a aplicação de técnicas baseadas em DFA (como minimização) a especificações LTL padrão.

Metodologia
O artigo apresenta uma tradução construtiva de fórmulas LTL arbitrárias para LLtf+ em tempo linear, assumindo que a fórmula LTL seja primeiro normalizada. A metodologia procede em três estágios principais:

1. Normalização para a Forma Normal $\Delta_2$:
   Os autores utilizam um sistema de reescrita de fórmulas puras (baseado em Esparza, Rubio e Sickert 2024) para traduzir qualquer fórmula LTL para a forma normal $\Delta_2$ (reatividade). Esta forma decompõe a fórmula em uma disjunção de termos, onde cada termo representa um "comportamento-limite" $(M, N)$ específico. Cada termo consiste em:

   • Uma fórmula de corpo $\Sigma_2$ simplificada ($\phi[M, N]$).
   • Verificações $\Pi_2$ para recorrência ($\bigwedge GF(\psi[N]_\mu)$).
   • Verificações $\Sigma_2$ para persistência ($\bigwedge FG(\psi[M]_\nu)$).
     Esta normalização é simples exponencial no tamanho da fórmula original.

2. Tradução de Blocos de Comportamento-Limite:
   O artigo define traduções específicas para as verificações de comportamento-limite em fórmulas folha de LTLf+:

   • Recorrência ($\Pi_2$): Fórmulas da forma $GF(\sigma_1)$ (onde $\sigma_1 \in \Sigma_1$) são traduzidas para $\forall\exists(F(\text{tight}(\text{finX}(\sigma_1))))$. Os autores introduzem um conceito de "completude estrita" (tight completion) usando um operador chop para garantir que a satisfação da fórmula esteja vinculada ao fim do prefixo, evitando a satisfação espúria em prefixos infinitos.
   • Persistência ($\Sigma_2$): Fórmulas da forma $FG(\pi_1)$ (onde $\pi_1 \in \Pi_1$) são traduzidas para $\exists\forall(G(\neg\text{tight}(\neg\text{finX}(\pi_1))))$.
   • Reinterpretação Finita: Os autores definem operadores finX e tight que reinterpretam os operadores LTL sobre traços finitos, distinguindo entre operadores next fortes e fracos com base no contexto (fragmentos de segurança vs. co-segurança).

3. Tradução de Corpos $\Sigma_2$:
   Para o corpo principal da fórmula normalizada ($\phi[M, N]$), os autores aproveitam o fato de que, sob um comportamento-limite $(M, N)$ fixo, todas as folhas de segurança (fórmulas G) eventualmente ocorrem para sempre. Ao projetar essas folhas de segurança para fora (substituindo-as por tt), o corpo da fórmula efetivamente reduz-se a uma fórmula $\Sigma_1$ (co-segurança). Os autores provam que, para traços exibindo o comportamento-limite específico, o corpo é "convergente", o que significa que sua satisfação em um traço infinito é equivalente à satisfação de sua reinterpretação finita em todos os mas não todos os prefixos. Isso permite que o corpo seja traduzido usando o quantificador existencial-universal: $\exists\forall(\text{finX}(\phi[M, N]))$.

Principais Contribuições

• Tradução Construtiva: O artigo fornece a primeira tradução construtiva de LTL geral para LTLf+, fechando a lacuna entre o resultado existencial de Aminof et al. (2025) e um algoritmo prático.
• Complexidade de Tradução Linear: A tradução da forma LTL normalizada para LTLf+ é linear no tamanho da fórmula normalizada.
• Preservação de Complexidade: O artigo demonstra que esta pipeline de tradução (LTL $\to$ Forma Normal $\to$ LTLf+ $\to$ DFA) permanece duplamente exponencial no tamanho da fórmula LTL original. Não introduz um aumento exponencial adicional em comparação com a tradução direta estado-da-arte de LTL para autômato.
• Viabilização de Técnicas de DFA: A tradução permite a aplicação de técnicas baseadas em DFA, como a minimização de autômatos, a problemas originalmente formulados em LTL. Isso é significativo porque DFAs podem ser minimizados eficientemente, enquanto minimizar autômatos de Büchi não determinísticos é PSPACE-completo.

Resultos
Os autores provam que, para cada fórmula LTL $\phi$ e traço infinito $w$, $w \models_{inf} \phi$ se, e somente se, $w \models_{inf} \text{Tradução}(\phi)$. A fórmula LTLf+ resultante é uma combinação booleana de fórmulas folha envolvendo quantificadores de prefixo ($\forall, \exists, \forall\exists, \exists\forall$) aplicados a reinterpretações de traço finito das subfórmulas originais. O comprimento da fórmula traduzida é limitado por $2^{O(|\phi|)}$, correspondendo ao tamanho da forma normal $\Delta_2$ intermediária.

Significância
O artigo estabelece a LTLf+ como uma linguagem intermediária prática para especificações LTL arbitrárias. Ao traduzir LTL para LTLf+, o ecossistema em expansão de técnicas eficientes baseadas em DFA desenvolvidas para lógica de traço finito torna-se disponível para problemas de traço infinito. Isso inclui:

• Síntese Reativa: Permitindo o uso de minimização de DFA para acelerar a síntese, uma capacidade anteriormente limitada a especificações de horizonte finito.
• Planejamento e Aprendizado: Estendendo a aplicabilidade dessas técnicas para processos de decisão de Markov, planejamento estocástico e aprendizado por reforço, onde objetivos LTL são utilizados.

Os autores observam que implementaram esta tradução sobre a biblioteca SPOT, incluindo otimizações para fragmentos específicos como obrigações, que podem pular a normalização e a completude estrita inteiramente. O trabalho posiciona a LTLf+ não apenas como uma extensão teórica, mas como um caminho de engenharia viável para melhorar a escalabilidade do raciocínio baseado em LTL na IA.