# LTLf+ and PPLTL+: Extending LTLf and PPLTL to Infinite Traces

arXiv: https://arxiv.org/abs/2411.09366 · HTML: https://mlsanity.com/paper/2411.09366/

## Key facts

- Cited by 4 papers in the map (data through 14 Oct 2026).
- Builds on 11 of its 67 references that are in the map.
- First posted on arXiv 14 Nov 2024.

## Builds on (most cited first, 11 of 11)

- [Graph Neural Networks Meet Neural-Symbolic Computing: A Survey and Perspective](https://mlsanity.com/paper/2003.00330/) (2020)
- [Hybrid Compositional Reasoning for Reactive Synthesis from Finite-Horizon Specifications](https://mlsanity.com/paper/1911.08145/) (2019)
- [Oink: an Implementation and Evaluation of Modern Parity Game Solvers](https://mlsanity.com/paper/1801.03859/) (2018)
- [Model Checking Strategies from Synthesis Over Finite Traces](https://mlsanity.com/paper/2305.08319/) (2023)
- [Reactive Synthesis from Extended Bounded Response LTL Specifications](https://mlsanity.com/paper/2008.05335/) (2020)
- [Live Synthesis](https://mlsanity.com/paper/2107.01136/) (2021)
- [Act for Your Duties but Maintain Your Rights](https://mlsanity.com/paper/2302.03384/) (2023)
- [Symbolic Solution of Emerson-Lei Games for Reactive Synthesis](https://mlsanity.com/paper/2305.02793/) (2023)
- [LTLf Best-Effort Synthesis in Nondeterministic Planning Domains](https://mlsanity.com/paper/2308.15188/) (2023)
- [LTLf Synthesis Under Environment Specifications for Reachability and Safety Properties](https://mlsanity.com/paper/2308.15184/) (2023)
- [Efficient Normalization of Linear Temporal Logic](https://mlsanity.com/paper/2310.12613/) (2023)

## Built on by (most cited first, 4 of 4)

- [Emerson-Lei and Manna-Pnueli Games for LTLf+ and PPLTL+ Synthesis](https://mlsanity.com/paper/2508.14725/) (2025)
- [Semantically Labelled Automata for Multi-Task Reinforcement Learning with LTL Instructions](https://mlsanity.com/paper/2602.06746/) (2026)
- [Symbolic Synthesis for LTLf+ Obligations](https://mlsanity.com/paper/2604.18532/) (2026)
- [Infinite Trace Objectives with Finite Trace Techniques: Translating LTL to LTLf+](https://mlsanity.com/paper/2608.02454/) (2026)

## Abstract (arXiv)

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