LTLf+ and PPLTL+: Extending LTLf and PPLTL to Infinite Traces
This work addresses the challenge of efficient reactive synthesis for infinite traces in formal verification, providing a novel approach that avoids the difficulties of determinizing infinite automata, though it builds incrementally on existing logics and hierarchies.
The authors tackled the problem of reactive synthesis for infinite traces by introducing LTLf+ and PPLTL+, which extend finite-trace logics to infinite traces while retaining expressive power equivalent to LTL. They achieved synthesis complexities of 2EXPTIME-complete for LTLf+ and EXPTIME-complete for PPLTL+, with the latter offering full LTL expressiveness at a lower complexity than typical LTL synthesis.
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+.