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

Technical Summary: Infinite Trace Objectives with Finite Trace Techniques

Problem Statement
Linear Temporal Logic (LTL) is the standard language for specifying temporal objectives in AI, ranging from reactive synthesis to planning in Markov decision processes. However, solving LTL-based problems traditionally requires translating an LTL formula into a nondeterministic automaton on infinite words and subsequently determinizing it. This determinization step is notoriously difficult, both theoretically and practically, creating a significant barrier to scalability. While recent advances in LTL synthesis utilize a normal form (based on the Manna-Pnueli safety-progress hierarchy) to decompose formulas into deterministic components, the translation from LTL to deterministic automata remains doubly exponential.

Concurrently, the logic LTLf (LTL on finite traces) has gained traction due to its ability to be translated efficiently into Deterministic Finite Automata (DFAs), which support efficient minimization. LTLf+ was recently introduced to lift LTLf to infinite traces by quantifying over prefixes, matching the Manna-Pnueli hierarchy classes. While LTLf+ possesses the same expressive power as LTL, a constructive translation from general LTL to LTLf+ was previously missing, limiting the application of DFA-based techniques (such as minimization) to standard LTL specifications.

Methodology
The paper presents a constructive translation from arbitrary LTL formulas to LTLf+ in linear time, assuming the LTL formula is first normalized. The methodology proceeds in three main stages:

1. Normalization to $\Delta_2$ Normal Form:
   The authors utilize a pure formula rewriting system (based on Esparza, Rubio, and Sickert 2024) to translate any LTL formula into the $\Delta_2$ (reactivity) normal form. This form decomposes the formula into a disjunction of terms, where each term represents a specific "limit-behavior" $(M, N)$. Each term consists of:

   • A simplified $\Sigma_2$ body formula ($\phi[M, N]$).
   • $\Pi_2$ checks for recurrence ($\bigwedge GF(\psi[N]_\mu)$).
   • $\Sigma_2$ checks for persistence ($\bigwedge FG(\psi[M]_\nu)$).
     This normalization is single exponential in the size of the original formula.

2. Translation of Limit-Behavior Blocks:
   The paper defines specific translations for the limit-behavior checks into LTLf+ leaf formulas:

   • Recurrence ($\Pi_2$): Formulas of the form $GF(\sigma_1)$ (where $\sigma_1 \in \Sigma_1$) are translated to $\forall\exists(F(\text{tight}(\text{finX}(\sigma_1))))$. The authors introduce a "tight completion" concept using a chop operator to ensure that the satisfaction of the formula is tied to the end of the prefix, preventing spurious satisfaction on infinite prefixes.
   • Persistence ($\Sigma_2$): Formulas of the form $FG(\pi_1)$ (where $\pi_1 \in \Pi_1$) are translated to $\exists\forall(G(\neg\text{tight}(\neg\text{finX}(\pi_1))))$.
   • Finite Reinterpretation: The authors define finX and tight operators that reinterpret LTL operators over finite traces, distinguishing between strong and weak next operators based on the context (safety vs. co-safety fragments).

3. Translation of $\Sigma_2$ Bodies:
   For the main body of the normalized formula ($\phi[M, N]$), the authors leverage the fact that under a fixed limit-behavior $(M, N)$, all safety leaves (G-formulas) eventually hold forever. By projecting these safety leaves out (replacing them with tt), the body formula effectively reduces to a $\Sigma_1$ (co-safety) formula. The authors prove that for traces exhibiting the specific limit-behavior, the body is "convergent," meaning its satisfaction on an infinite trace is equivalent to the satisfaction of its finite reinterpretation on all but finitely many prefixes. This allows the body to be translated using the existential-universal quantifier: $\exists\forall(\text{finX}(\phi[M, N]))$.

Key Contributions

• Constructive Translation: The paper provides the first constructive translation from general LTL to LTLf+, closing the gap between the existential result of Aminof et al. (2025) and a practical algorithm.
• Linear Translation Complexity: The translation from the normalized LTL form to LTLf+ is linear in the size of the normalized formula.
• Preservation of Complexity: The paper demonstrates that this translation pipeline (LTL $\to$ Normal Form $\to$ LTLf+ $\to$ DFA) remains doubly exponential in the size of the original LTL formula. It does not introduce an additional exponential blow-up compared to the state-of-the-art direct LTL-to-automaton translation.
• Enabling DFA Techniques: The translation enables the application of DFA-based techniques, such as automaton minimization, to problems originally formulated in LTL. This is significant because DFAs can be minimized efficiently, whereas minimizing nondeterministic Büchi automata is PSPACE-complete.

Results
The authors prove that for every LTL formula $\phi$ and infinite trace $w$, $w \models_{inf} \phi$ if and only if $w \models_{inf} \text{Translation}(\phi)$. The resulting LTLf+ formula is a Boolean combination of leaf formulas involving prefix quantifiers ($\forall, \exists, \forall\exists, \exists\forall$) applied to finite-trace reinterpretations of the original subformulas. The length of the translated formula is bounded by $2^{O(|\phi|)}$, matching the size of the intermediate $\Delta_2$ normal form.

Significance
The paper establishes LTLf+ as a practical intermediate language for arbitrary LTL specifications. By translating LTL to LTLf+, the expanding ecosystem of efficient DFA-based techniques developed for finite-trace logic becomes available for infinite-trace problems. This includes:

• Reactive Synthesis: Allowing the use of DFA minimization to speed up synthesis, a capability previously limited to finite-horizon specifications.
• Planning and Learning: Extending the applicability of these techniques to Markov decision processes, stochastic planning, and reinforcement learning where LTL objectives are used.

The authors note that they have implemented this translation on top of the SPOT library, including optimizations for specific fragments like obligations, which can skip normalization and tight completion entirely. The work positions LTLf+ not just as a theoretical extension, but as a viable engineering pathway to improve the scalability of LTL-based reasoning in AI.