{"ID":2842675,"CreatedAt":"2026-06-01T04:54:23.091178241Z","UpdatedAt":"2026-06-01T04:54:23.091178241Z","DeletedAt":null,"paper_url":"https://arxiv.org/abs/2511.09073","arxiv_id":"2511.09073","title":"Good-for-MDP State Reduction for Stochastic LTL Planning","abstract":"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}\\varphi$, 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.","short_abstract":"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, allowin...","url_abs":"https://arxiv.org/abs/2511.09073","url_pdf":"https://arxiv.org/pdf/2511.09073v2","authors":"[\"Christoph Weinhuber\",\"Giuseppe De Giacomo\",\"Yong Li\",\"Sven Schewe\",\"Qiyi Tang\"]","published":"2025-11-12T07:48:09Z","proceeding":"cs.FL","tasks":"[\"cs.FL\",\"cs.AI\",\"cs.GT\"]","methods":"[]","has_code":false}