# Good-for-MDP State Reduction for Stochastic LTL Planning

arXiv: https://arxiv.org/abs/2511.09073 · HTML: https://mlsanity.com/paper/2511.09073/

## Key facts

- Cited by 3 papers in the map (data through 14 Oct 2026).
- Builds on 4 of its 47 references that are in the map.
- First posted on arXiv 12 Nov 2025.

## Builds on (most cited first, 4 of 4)

- [An Efficient Normalisation Procedure for Linear Temporal Logic and Very Weak Alternating Automata](https://mlsanity.com/paper/2005.00472/) (2020)
- [Solving MDPs with LTLf+ and PPLTL+ Temporal Objectives](https://mlsanity.com/paper/2505.17264/) (2025)
- [Minimization and Canonization of GFG Transition-Based Automata](https://mlsanity.com/paper/2106.06745/) (2021)
- [Planning with Linear Temporal Logic Specifications: Handling Quantifiable and Unquantifiable Uncertainty](https://mlsanity.com/paper/2502.19603/) (2025)

## Built on by (most cited first, 3 of 3)

- [Semantically Labelled Automata for Multi-Task Reinforcement Learning with LTL Instructions](https://mlsanity.com/paper/2602.06746/) (2026)
- [Multi-Property Synthesis](https://mlsanity.com/paper/2601.10651/) (2026)
- [Infinite Trace Objectives with Finite Trace Techniques: Translating LTL to LTLf+](https://mlsanity.com/paper/2608.02454/) (2026)

## Abstract (arXiv)

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 mathsfGmathsfFvarphi, where varphi 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.