Search papers, labs, and topics across Lattice.
This paper introduces a novel translation from Linear Temporal Logic (LTL) to LTLf+, enabling the use of finite automata techniques for problems traditionally tackled with LTL. By normalizing LTL formulas into the syntactic reactivity fragment of the Manna-Pnueli hierarchy, the authors provide linear translations for each component, facilitating the application of efficient LTLf+ methods to a broader range of AI problems. Importantly, this translation maintains the same asymptotic complexity, ensuring that the benefits of LTLf+ can be leveraged without compromising performance.
Translating LTL to LTLf+ unlocks efficient finite automata techniques for a wide array of AI applications without sacrificing complexity.
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.
