Solving MDPs with LTLf+ and PPLTL+ Temporal Objectives

De Giacomo, Giuseppe; Li, Yong; Schewe, Sven; Weinhuber, Christoph; Yu, Pian

doi:10.24963/ijcai.2025/944

Solving MDPs with LTLf+ and PPLTL+ Temporal Objectives

Giuseppe De Giacomo, Yong Li, Sven Schewe, Christoph Weinhuber, Pian Yu

Download BibTeX Cite

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

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

Keywords

Planning and Scheduling: PS: Markov decisions processes
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

Abstract

The temporal logics LTLf+ and PPLTL+ have recently been introduced to express objectives over infinite traces. These logics are appealing because they match the expressive power of LTL on infinite traces while enabling efficient DFA-based techniques, which have been crucial to the scalability of reactive synthesis and adversarial planning in LTLf and PPLTL over finite traces. In this paper, we demonstrate that these logics are also highly effective in the context of MDPs. Introducing a technique tailored for probabilistic systems, we leverage the benefits of efficient DFA-based methods and compositionality. This approach is simpler than its nonprobabilistic counterparts in reactive synthesis and adversarial planning, as it accommodates a controlled form of nondeterminism ("good for MDPs") in the automata when transitioning from finite to infinite traces. Notably, by exploiting compositionality, our solution is both implementation-friendly and well-suited for straightforward symbolic implementations.

Giuseppe De Giacomo, Yong Li, Sven Schewe, Christoph Weinhuber, and Pian Yu. 2025. Solving MDPs with LTLf+ and PPLTL+ Temporal Objectives. In Proceedings of the Thirty-Fourth International Joint Conference on Artificial Intelligence, IJCAI-25. IJCAI, 8491–8499. https://doi.org/10.24963/ijcai.2025/944

@inproceedings{ijcai2025p944,
  title     = {Solving MDPs with LTLf+ and PPLTL+ Temporal Objectives},
  author    = {De Giacomo, Giuseppe and Li, Yong and Schewe, Sven and Weinhuber, Christoph and Yu, Pian},
  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     = {8491--8499},
  year      = {2025},
  month     = {8},
  note      = {Main Track},
  doi       = {10.24963/ijcai.2025/944},
  url       = {https://doi.org/10.24963/ijcai.2025/944},
}

TY  - CPAPER
TI  - Solving MDPs with LTLf+ and PPLTL+ Temporal Objectives
AU  - De Giacomo, Giuseppe
AU  - Li, Yong
AU  - Schewe, Sven
AU  - Weinhuber, Christoph
AU  - Yu, Pian
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  - 8491
EP  - 8499
DO  - 10.24963/ijcai.2025/944
UR  - https://doi.org/10.24963/ijcai.2025/944
ER  -