扩展有限轨迹逻辑，让无限轨迹性质表达更高效且可合成。
LTLf+ and PPLTL+: Extending LTLf and PPLTL to Infinite Traces
- 基于安全-进展层级构建新逻辑，保留原逻辑的策略提取机制。
- LTLf+合成为2EXPTIME完备，PPLTL+为EXPTIME完备，效率提升显著。
- 适合形式化验证与自动合成研究者，尤其关注复杂度优化者。
我们引入LTLf+和PPLTL+两种逻辑，用于表达无限轨迹上的性质，其基础是有限轨迹上的线性时序逻辑LTLf和PPLTL。LTLf+/PPLTL+采用Manna和Pnueli的LTL安全-进展层次结构，因此具有与LTL相同的表达能力。然而，它们仍保持原始逻辑在反应式合成问题中的关键特性：策略提取的游戏场景可由确定性有限自动机（DFA）导出。因此，这些逻辑避开了传统LTL合成中无限轨迹自动机确定化的难题。我们提出了基于DFA的合成技术，证明了LTLf+合成为2EXPTIME完全（与LTLf一致），而PPLTL+为EXPTIME完全（与PPLTL一致）。值得注意的是，尽管PPLTL+具备完整的LTL表达能力，其合成复杂度为EXPTIME完全而非2EXPTIME完全。这些技术还被拓展用于最优求解可满足性、有效性及模型检验，得到LTLf+为EXPSPACE完全（扩展了近期关于保证级使用LTLf的结果），PPLTL+为PSPACE完全。
原文摘要 · Abstract (English)
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+.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。