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 minima
用有限轨迹技术实现 LTL 的无限轨迹目标。
- 核心方法
- 引入了 LTLf+，将有限轨迹逻辑 LTLf 扩展到无限轨迹，利用有限自动机技术处理无限轨迹目标，简化了 LTL 的处理流程。
- 适合谁读
- 研究者
- 要解决的问题
- 传统使用 LTL 指定无限轨迹目标时需要将其转换为非确定性无限自动机并确定化，这在理论上和实践中都非常困难。
- 关键实验
- 未提供
- 主要贡献
- LTLf+ 保留了 LTL 的表达能力，同时利用了 LTLf 的优势，主要基于有限迹自动机进行推理，提供了更简洁有效的解决方案。
- 意义与局限
- 该方法简化了无限轨迹目标在 AI 问题（如反应合成、马尔科夫决策过程中的随机规划和强化学习）中的处理，但其具体应用效果还需进一步验证。