mlsanityData to 14 Oct 2026

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

arXiv 2608.02454 ↗First posted 3 Aug 2026cs.AI cs.FL cs.LOcited by 0

On the map: Deep reinforcement learning methods → Interpretable and logic-guided RL

Abstract (arXiv)

Linear Temporal Logic (LTL) is one of the most widely adopted languages for specifying temporal extended objectives in AI, with applications ranging from reactive synthesis to stochastic planning in Markov decision processes and reinforcement learning. Traditionally, solving any of these problems requires translating the LTL specification to a nondeterministic automata on infinite words and then determinizing it, a step that is notoriously difficult in theory and in practice. Recent work has introduced LTLf+, which lifts the finite-trace logic LTLf to infinite traces. LTLf+ has the same expressive power as LTL, yet it retains most of the crucial advantages of its base logic LTLf. Most reasoning in LTLf+ rests on finite automata on finite words, for which we have not only a canonical minimal representation but also an efficient determinization procedure. In this work we present the first translation from LTL to LTLf+. We first normalize an LTL formula into the syntactic reactivity fragment of the Manna-Pnueli hierarchy, to create the general fragment-based shape of LTLf+. We then present linear translations for each individual component of that fragment. As a consequence of this translation, the expanding body of techniques developed for LTLf+ now becomes available to many AI problems currently formulated in LTL. We further show that this comes at no asymptotic cost, as the pipeline from LTL to automaton via LTLf+ remains doubly exponential.

Key facts. No citing papers in the map yet (data through 14 Oct 2026). Placed in Interpretable and logic-guided RL, one of 15 directions in Deep reinforcement learning methods. Builds on 9 of its 35 references that are in the map. First posted on arXiv 3 Aug 2026.

Builds on

9 of 35 references.

Closest ancestors · 1

Same direction, newest first

  1. 2026Semantically Labelled Automata for Multi-Task Reinforcement Learning with LTL Instructions6 Feb

Other references · 8

  1. 2019Hybrid Compositional Reasoning for Reactive Synthesis from Finite-Horizon Specificationscited by 16
  2. 2025SemML: Enhancing Automata-Theoretic LTL Synthesis with Machine Learningcited by 6
  3. 2024LTLf+ and PPLTL+: Extending LTLf and PPLTL to Infinite Tracescited by 4
  4. 2025Solving MDPs with LTLf+ and PPLTL+ Temporal Objectivescited by 3
  5. 2025Good-for-MDP State Reduction for Stochastic LTL Planningcited by 3
  6. 2025Emerson-Lei and Manna-Pnueli Games for LTLf+ and PPLTL+ Synthesiscited by 2
  7. 2026Symbolic Synthesis for LTLf+ Obligationscited by 1
  8. 2026SemML 2.0: Synthesizing Controllers for LTLcited by 1

Built on by

Not cited yet.

Similar, not cited

Close in wording, no citation either way

  1. 2024DeepLTL: Learning to Efficiently Satisfy Complex LTL Specifications for Multi-Task RL
  2. 2026PlatoLTL: Scaling LTL-Guided Multi-Task RL
  3. 2026Do It for HER: First-Order Temporal Logic Reward Specification in Reinforcement Learning (Extended Version)
  4. 2026hint2: Hierarchical World Models for Inference-Time Temporal Logic Guidance
  5. 2025Learning Probabilistic Temporal Logic Specifications for Stochastic Systems
  6. 2024Comp-LTL: Temporal Logic Planning via Zero-Shot Policy Composition
  7. 2026LTLGuard: Formalizing LTL Specifications with Compact Language Models and Lightweight Symbolic Reasoning
  8. 2024LTLBench: Towards Benchmarks for Evaluating Temporal Reasoning in Large Language Models