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

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

doi:10.24963/ijcai.2025/939

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

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

Download BibTeX Cite

Proceedings of the Thirty-Fourth International Joint Conference on Artificial Intelligence. Main Track. Pages 8447-8455.

https://doi.org/10.24963/ijcai.2025/939

Keywords

Agent-based and Multi-agent Systems: MAS: Formal verification, validation and synthesis
Planning and Scheduling: PS: Theoretical foundations of planning
Knowledge Representation and Reasoning: KRR: Reasoning about actions

Abstract

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.

Benjamin Aminof, Giuseppe De Giacomo, Sasha Rubin, and Moshe Y. Vardi. 2025. LTLf+ and PPLTL+: Extending LTLf and PPLTL to Infinite Traces. In Proceedings of the Thirty-Fourth International Joint Conference on Artificial Intelligence, IJCAI-25. IJCAI, 8447–8455. https://doi.org/10.24963/ijcai.2025/939

@inproceedings{ijcai2025p939,
  title     = {LTLf+ and PPLTL+: Extending LTLf and PPLTL to Infinite Traces},
  author    = {Aminof, Benjamin and De Giacomo, Giuseppe and Rubin, Sasha and Vardi, Moshe Y.},
  booktitle = {Proceedings of the Thirty-Fourth International Joint Conference on
               Artificial Intelligence, {IJCAI-25}},
  publisher = {International Joint Conferences on Artificial Intelligence Organization},
  editor    = {James Kwok},
  pages     = {8447--8455},
  year      = {2025},
  month     = {8},
  note      = {Main Track},
  doi       = {10.24963/ijcai.2025/939},
  url       = {https://doi.org/10.24963/ijcai.2025/939},
}

TY  - CPAPER
TI  - LTLf+ and PPLTL+: Extending LTLf and PPLTL to Infinite Traces
AU  - Aminof, Benjamin
AU  - De Giacomo, Giuseppe
AU  - Rubin, Sasha
AU  - Vardi, Moshe Y.
T2  - Proceedings of the Thirty-Fourth International Joint Conference on Artificial Intelligence, IJCAI-25
PB  - International Joint Conferences on Artificial Intelligence Organization
PY  - 2025
SP  - 8447
EP  - 8455
DO  - 10.24963/ijcai.2025/939
UR  - https://doi.org/10.24963/ijcai.2025/939
ER  -