Solving MDPs with LTLf+ and PPLTL+ Temporal Objectives
Authors: Giuseppe De Giacomo, Yong Li, Sven Schewe, Christoph Weinhuber, Pian Yu
IJCAI 2025 | Venue PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Theoretical | In this paper, we investigated the problem of solving MDPs with LTLf+ and PPLTL+ temporal objectives, showing the effectiveness of these logics for probabilistic planning in MDPs. Our key contribution lies in presenting a provably correct technique to construct GFM B uchi automata for LTLf+ and PPLTL+ formulas, leveraging the compositional advantages of DFA-based methods. Note that our construction is designed to be implementation-friendly and well-suited for a straightforward symbolic implementation. In fact, for PPLTL we can directly construct the symbolic DFA in polynomial time [De Giacomo et al., 2020]. The final Boolean combination of these symbolic B uchi automata, as described in Section 4.2, is at most polynomial in their combined sizes and can be realised through a Cartesian product. As a future work, we aim to implement this approach, employing symbolic techniques, within state-of-the-art tools such as PRISM [Kwiatkowska et al., 2011]. This development will facilitate the practical application of our methods across a range of domains, including AI, robotics, and probabilistic verification. |
| Researcher Affiliation | Academia | 1 Department of Computer Science, University of Oxford, UK 2 Key Laboratory of System Software (Chinese Academy of Sciences) and State Key Laboratory of Computer Science, Institute of Software Chinese Academy of Sciences, PRC 3 Department of Computer Science, University of Liverpool, UK 4 Department of Computer Science, University College London, UK |
| Pseudocode | No | The paper describes methods through detailed textual explanations and theorems, such as in Section 4.1 'Construction for ϕ, ϕ, ϕ, and ϕ', which outlines steps in prose rather than using formal pseudocode or algorithm blocks. For example: '1. First, let D = (Σ, Q, ι, δ, F) be DFA(ϕ) such that L (D) = [ϕ]. 2. Second, make all final states in F sink final states, i.e., δ(s, a) = s for each s F and a Σ, obtaining the automaton C = (Q, ι , δ , F ). C remains deterministic. 3. Finally, read it as DBA B = (Q, ι , δ , F ).' |
| Open Source Code | No | As a future work, we aim to implement this approach, employing symbolic techniques, within state-of-the-art tools such as PRISM [Kwiatkowska et al., 2011]. This development will facilitate the practical application of our methods across a range of domains, including AI, robotics, and probabilistic verification. This indicates that code implementation is planned for the future, not currently available. |
| Open Datasets | No | This is a theoretical paper focusing on formalisms, logic, and automaton constructions for solving MDPs. It does not describe experiments that use or evaluate specific datasets. |
| Dataset Splits | No | This is a theoretical paper that does not conduct experiments involving datasets or their splits. Therefore, no training/test/validation splits are provided. |
| Hardware Specification | No | This is a theoretical paper presenting formal methods and constructions, not empirical experiments. As such, no hardware specifications for running experiments are provided. |
| Software Dependencies | No | The paper is theoretical and does not report on any software used for experiments. While PRISM [Kwiatkowska et al., 2011] is mentioned, it is in the context of future work for implementation: 'As a future work, we aim to implement this approach, employing symbolic techniques, within state-of-the-art tools such as PRISM'. |
| Experiment Setup | No | This is a theoretical paper that does not involve experimental setups, hyperparameters, or training configurations. |