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+.

翻译：本文提出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完全性。