AI 中文总结
本研究提出首个从LTL到LTLf+的线性转换方法，将LTL归一化为Manna-Pnueli层次的反应片段，保留LTLf+的优势且无渐近代价，可将LTLf+技术应用于更多AI问题。
AI 中文摘要
线性时序逻辑（LTL）是AI中应用最广泛的语言之一，用于指定时间扩展目标，应用范围涵盖反应式综合、马尔可夫决策过程中的随机规划以及强化学习。传统上，解决这些问题需要将LTL规范转换为无限字上的非确定性自动机，随后对其进行确定化，这一步骤在理论和实践中都极具难度。近期研究引入了LTLf+，它将有限迹逻辑LTLf扩展至无限迹，其表达能力与LTL相当，同时保留了基础逻辑LTLf的大部分关键优势。LTLf+中的大部分推理依赖于有限字上的有限自动机，这类自动机不仅具有规范的最小表示，还拥有高效的确定化过程。在本研究中，我们提出了首个从LTL到LTLf+的转换方法：首先将LTL公式归一化为Manna-Pnueli层次的语法反应片段，以构建LTLf+通用的片段化结构；随后为该片段的每个单独组件提供线性转换。这一转换的结果是，目前针对LTLf+开发的大量技术可应用于许多当前以LTL形式表述的AI问题。我们进一步证明，该转换无渐近代价，因为从LTL经LTLf+到自动机的 pipeline 仍保持双指数复杂度。
英文摘要
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.
