这篇论文把LTL规约转成LTLf+，以后处理无限迹目标就能用有限自动机的成熟工具了，而且复杂度不涨。
本文提出首个从线性时序逻辑LTL到LTLf+的翻译方法，LTLf+是一种保留LTL表达能力的无限迹逻辑，但推理可基于有限字上的有限自动机。作者先将LTL公式归一化为Manna-Pnueli层次中的语法反应性片段，再对该片段各组件给出线性翻译。该翻译使LTLf+的有限自动机技术可用于AI中的LTL问题，且从LTL经LTLf+到自动机的整体复杂度保持双重指数，无额外渐近代价。
Infinite Trace Objectives with Finite Trace Techniques: Translating LTL to LTLf+
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.