LTLf+ 和 PPLTL+：将 LTLf 和 PPLTL 扩展至无穷迹
LTLf+ and PPLTL+: Extending LTLf and PPLTL to Infinite Traces
AI总结：
本文提出 LTLf+ 和 PPLTL+ 逻辑以表达无穷迹性质，利用 DFA 推导策略提取的博弈竞技场，规避了 LTL 反应式综合中自动机确定化的困难，并证明了其综合、可满足性等问题的计算复杂度。
摘要：
我们引入了 LTLf+ 和 PPLTL+ 这两种表达无穷迹性质的逻辑，它们基于有限迹上的线性时序逻辑 LTLf 和 PPLTL。LTLf+/PPLTL+ 使用了 Manna 和 Pnueli 的 LTL 安全性-进展性层级，因此具有与 LTL 相同的表达能力。然而，它们也保留了基础逻辑反应式综合问题的一个关键特征：用于策略提取的博弈竞技场可以从确定性有限自动机（DFA）推导得出。因此，这些逻辑规避了 LTL 反应式综合中典型的、与无穷迹自动机确定化相关的臭名昭著的困难。我们提出了基于 DFA 的 LTLf+/PPLTL+ 综合技术，并表明 LTLf+ 的综合是 2EXPTIME 完全的（与 LTLf 匹配），PPLTL+ 的综合是 EXPTIME 完全的（与 PPLTL 匹配）。值得注意的是，尽管 PPLTL+ 保留了 LTL 的全部表达能力，其反应式综合是 EXPTIME 完全的，而非 2EXPTIME 完全的。这些技术也适用于最优地解决可满足性、有效性和模型检测问题，使得 LTLf+ 为 EXPSPACE 完全的（扩展了最近使用 LTLf 针对保证级别的结果），PPLTL+ 为 PSPACE 完全的。
英文摘要：
We introduce LTLf+ and PPLTL+, two logics to express properties of infinite traces, that are based on the linear-time temporal logics LTLf and PPLTL on finite traces. LTLf+/PPLTL+ use levels of Manna and Pnueli's LTL safety-progress hierarchy, and thus have the same expressive power as LTL. However, they also retain a crucial characteristic of the reactive synthesis problem for the base logics: the game arena for strategy extraction can be derived from deterministic finite automata (DFA). Consequently, these logics circumvent the notorious difficulties associated with determinizing infinite trace automata, typical of LTL reactive synthesis. We present DFA-based synthesis techniques for LTLf+/PPLTL+, and show that synthesis is 2EXPTIME-complete for LTLf+ (matching LTLf) and EXPTIME-complete for PPLTL+ (matching PPLTL). Notably, while PPLTL+ retains the full expressive power of LTL, reactive synthesis is EXPTIME-complete instead of 2EXPTIME-complete. The techniques are also adapted to optimally solve satisfiability, validity, and model-checking, to get EXPSPACE-complete for LTLf+ (extending a recent result for the guarantee level using LTLf), and PSPACE-complete for PPLTL+.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
