Infinite Trace Objectives with Finite Trace Techniques: Translating LTL to LTLf+
2026-08-03 • Artificial Intelligence
Artificial IntelligenceFormal Languages and Automata TheoryLogic in Computer Science
AI summaryⓘ
The authors focus on a logic called Linear Temporal Logic (LTL), which is used in AI for tasks like planning and decision-making over time. Normally, working with LTL involves a tough step called determinization that is complex. They introduce a new way to convert LTL formulas into a related logic called LTLf+, which keeps the same abilities but uses easier-to-handle automata. Their method breaks down LTL into simpler pieces and then translates each piece efficiently. This approach allows existing LTLf+ tools to be applied to problems originally stated in LTL without making the process more complicated in terms of speed.
Linear Temporal Logic (LTL)LTLf+Automata theoryDeterminizationFinite automataManna-Pnueli hierarchyReactive synthesisMarkov decision processesReinforcement learningTemporal logic
Authors
Christoph Weinhuber, Maximilian Prokop, Giuseppe De Giacomo, Moshe Y. Vardi
Abstract
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.