Good-for-MDP State Reduction for Stochastic LTL Planning
Fuente:
arXiv
Saved in:
| Main Authors: | , , , , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866912710002737152 |
|---|---|
| author | Weinhuber, Christoph De Giacomo, Giuseppe Li, Yong Schewe, Sven Tang, Qiyi |
| author_facet | Weinhuber, Christoph De Giacomo, Giuseppe Li, Yong Schewe, Sven Tang, Qiyi |
| contents | We study stochastic planning problems in Markov Decision Processes (MDPs) with goals specified in Linear Temporal Logic (LTL). The state-of-the-art approach transforms LTL formulas into good-for-MDP (GFM) automata, which feature a restricted form of nondeterminism. These automata are then composed with the MDP, allowing the agent to resolve the nondeterminism during policy synthesis. A major factor affecting the scalability of this approach is the size of the generated automata. In this paper, we propose a novel GFM state-space reduction technique that significantly reduces the number of automata states. Our method employs a sophisticated chain of transformations, leveraging recent advances in good-for-games minimisation developed for adversarial settings. In addition to our theoretical contributions, we present empirical results demonstrating the practical effectiveness of our state-reduction technique. Furthermore, we introduce a direct construction method for formulas of the form $\mathsf{G}\mathsf{F}φ$, where $φ$ is a co-safety formula. This construction is provably single-exponential in the worst case, in contrast to the general doubly-exponential complexity. Our experiments confirm the scalability advantages of this specialised construction. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2511_09073 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Good-for-MDP State Reduction for Stochastic LTL Planning Weinhuber, Christoph De Giacomo, Giuseppe Li, Yong Schewe, Sven Tang, Qiyi Formal Languages and Automata Theory Artificial Intelligence Computer Science and Game Theory F.4.3; I.2.4; I.2.8 We study stochastic planning problems in Markov Decision Processes (MDPs) with goals specified in Linear Temporal Logic (LTL). The state-of-the-art approach transforms LTL formulas into good-for-MDP (GFM) automata, which feature a restricted form of nondeterminism. These automata are then composed with the MDP, allowing the agent to resolve the nondeterminism during policy synthesis. A major factor affecting the scalability of this approach is the size of the generated automata. In this paper, we propose a novel GFM state-space reduction technique that significantly reduces the number of automata states. Our method employs a sophisticated chain of transformations, leveraging recent advances in good-for-games minimisation developed for adversarial settings. In addition to our theoretical contributions, we present empirical results demonstrating the practical effectiveness of our state-reduction technique. Furthermore, we introduce a direct construction method for formulas of the form $\mathsf{G}\mathsf{F}φ$, where $φ$ is a co-safety formula. This construction is provably single-exponential in the worst case, in contrast to the general doubly-exponential complexity. Our experiments confirm the scalability advantages of this specialised construction. |
| title | Good-for-MDP State Reduction for Stochastic LTL Planning |
| topic | Formal Languages and Automata Theory Artificial Intelligence Computer Science and Game Theory F.4.3; I.2.4; I.2.8 |
| url | https://arxiv.org/abs/2511.09073 |