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

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

Benjamin Aminof, Giuseppe De Giacomo, Sasha Rubin, Moshe Y. Vardi

Proceedings of the Thirty-Fourth International Joint Conference on Artificial Intelligence
Main Track. Pages 8447-8455. https://doi.org/10.24963/ijcai.2025/939

We study two logics, LTLf+ and PPLTL+, 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 reactive synthesis 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 synthesis. We present optimal DFA-based technique for solving reactive synthesis for LTLf+ and PPLTL+. Additionally, we adapt these algorithms to optimally solve satisfiability and model-checking for these two logics.
Keywords:
Planning and Scheduling: PS: Theoretical foundations of planning
Knowledge Representation and Reasoning: KRR: Reasoning about actions
Agent-based and Multi-agent Systems: MAS: Formal verification, validation and synthesis