analiza aiqbench
This research introduces the first translation method from Linear Temporal Logic (LTL) to LTLf+, enabling AI systems to leverage efficient finite-trace reasoning techniques for infinite-horizon problems like reinforcement learning. By normalizing formulas into specific fragments, the approach eliminates the traditionally difficult determinization of nondeterministic automata on infinite words without increasing asymptotic complexity. Consequently, a vast array of existing tools developed for LTLf+ can now be directly applied to standard AI planning and synthesis tasks formulated in LTL.
Infinite Trace Objectives with Finite Trace Techniques: Translating LTL to LTLf+
arXiv:2608.02454v1 Announce Type: new 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.
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.
Artificial Intelligence (cs.AI); Formal Languages and Automata Theory (cs.FL); Logic in Computer Science (cs.LO)
arXiv:2608.02454 [cs.AI]
(or arXiv:2608.02454v1 [cs.AI] for this version)
https://doi.org/10.48550/arXiv.2608.02454 Focus to learn more arXiv-issued DOI via DataCite (pending registration)
arXivLabs is a framework that allows collaborators to develop and share new arXiv features directly on our website.
Both individuals and organizations that work with arXivLabs have embraced and accepted our values of openness, community, excellence, and user data privacy. arXiv is committed to these values and only works with partners that adhere to them.
Have an idea for a project that will add value for arXiv's community? Learn more about arXivLabs.
Text integral sub licența deschisă a publicației · 329 cuvinte
Subiecte conexe
Generalization and infinite width
LessWrong · 1 aug. 2026
Lattice-Based Cryptography Explained
Quantum Zeitgeist · 15 aug. 2026
When Automata Meet Streams: Temporal Logic Compilation for Stream-Based Robotics Task and Motion Planning
arXiv · 21 aug. 2026
Runway’s WorldPrompt and the Engineering of Real-Time Worlds
Latent Space · 25 sept. 2026