Good-for-MDP State Reduction for Stochastic LTL Planning

TL;DR

This paper introduces a novel state-space reduction technique for good-for-MDP automata used in stochastic LTL planning, significantly improving scalability and efficiency in policy synthesis.

Contribution

We propose a new GFM automata state reduction method leveraging recent minimisation advances and a specialized construction for G F formulas, enhancing scalability in stochastic LTL planning.

Findings

Automata state reduction leads to more scalable planning.

Specialized G F formula construction is single-exponential.

Empirical results confirm improved scalability.

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.