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
