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

TL;DR

This paper introduces LTLf+ and PPLTL+ logics for infinite traces, enabling automata-based synthesis with complexity matching their base logics, and simplifies reactive synthesis by avoiding infinite automata determinization.

Contribution

It extends LTLf and PPLTL to infinite traces, maintaining automata-based synthesis and complexity bounds, and simplifies reactive synthesis by leveraging DFA-based strategies.

Findings

Synthesis complexity is 2EXPTIME for LTLf+ and EXPTIME for PPLTL+.

Automata-based synthesis techniques are adapted for the new logics.

Satisfiability, validity, and model-checking complexities are established.

Abstract

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