Skip to content

Good-for-MDP State Reduction for Stochastic LTL Planning

🕒 Published (v1): 2025-11-12 07:48 UTC · Source: Arxiv · Venue: AAAI 2026 · link

Ask a follow-up

Open an assistant pre-loaded with this paper's context.

💬 Ask ChatGPT✦ Ask Claude

TL;DR

This paper proposes a state-space reduction technique for good-for-MDP (GFM) automata used in stochastic LTL planning over MDPs, significantly shrinking the automata that encode task specifications. It also provides a direct, singly-exponential GFM construction for the common GFφ formula fragment, versus the doubly-exponential general case.

Problem

Solving MDPs with LTL goals requires composing the MDP with a GFM automaton encoding the specification; scalability is bottlenecked by automaton size. Existing LTL-to-GFM constructions (Owl, "slim") produce automata that are doubly-exponential in formula size, and no general minimization technique existed for the GFM class.

Method

A four-step polynomial-time Redux pipeline reduces any GFM Büchi automaton to a compact 0/1-probabilistic automaton (0/1-PA): 1. GFM → DBA: Embed nondeterministic transition choices [k] into the alphabet, yielding a deterministic Büchi automaton (DBA) of the same state count. 2. DBA → DCA: Syntactically reinterpret the acceptance condition (constant-time flip to co-Büchi). 3. DCA → GFG-NCA (minimized): Apply the polynomial good-for-games co-Büchi minimization algorithm of Radi & Kupferman (2022), which applies because the DCA is trivially GFG. 4. GFG-NCA → 0/1-PA: Resolve nondeterminism uniformly at random; a result from Li et al. (2025) guarantees language equivalence and the 0/1 acceptance property.

The paper proves that optimal strategy synthesis on the product MDP⊗0/1-PA recovers the true maximal LTL satisfaction probability. Separately, for formulas GFφ (φ co-safety), a direct NFA-based construction yields a GFM automaton with 2^O(|φ|) states instead of 2^2^O(|φ|).

Key Contributions

  • Polynomial Redux pipeline converting any GFM automaton to a semantically equivalent, minimized 0/1-PA, proven to preserve optimal MDP strategies (Theorem 4).
  • First formal proof that 0/1-PAs constitute a GFM automaton class (Theorem 2).
  • Direct singly-exponential GFM construction for GFφ (repeated reachability) with proven correctness and complexity (Theorem 5).
  • Empirical validation on benchmarks drawn from 8+ sources (planning, verification, RL).

Results

  • General reduction (Table 1): Across all patterns, reduced automata (Owl-Red, Slim-Red) are consistently the smallest.
  • BRP[6]: Owl=69 states → Owl-Red=17; Slim=317 → Slim-Red=65.
  • NU[6]: Owl=433 → Owl-Red=249 (27.75s reduction); Slim=1425 → Slim-Red=753 (163s).
  • Direct GFφ construction (Table 2): GFM-GF dominates for TDR and LIB patterns.
  • TDR[10]: GFM-GF=11 states (0.09s) vs. Owl-Red=1024 states (23.67s) vs. Slim-Red=514 states (0.91s).
  • LIB[7]–LIB[9]: Slim-Red times out (>300s); GFM-GF produces 15–19 states in <0.25s.
  • Owl-Red generally outperforms Slim-Red for non-GFφ patterns (BRP, EHP, NU, LIB).

Limitations

  • The Redux pipeline's effectiveness depends on the quality of the GFG co-Büchi minimizer (SPOT); worst-case reduction may be limited.
  • GFG co-Büchi minimization is polynomial but can be slow in practice (some NU and LIB reductions take tens of seconds).
  • The direct GFφ construction only applies to the syntactic GFφ fragment; general LTL formulas still use Redux.
  • No end-to-end planning experiment is included—only automaton size and construction time are benchmarked; downstream MDP solving time is not measured.
  • Doubly-exponential blowup during initial GFM construction (before reduction) remains unavoidable for general LTL.

Relevance to Agentic AI / LLM Agents

This work is formal-methods research rather than LLM research, but it is directly relevant to agents that use LTL for task specification: GFM automata underpin reward-machine-style RL (e.g., DeepLTL at ICLR 2025) and MDP-based planning with non-Markovian objectives, both active directions for LLM-augmented agents. Smaller automata mean smaller product MDPs, reducing the cost of policy synthesis in any agent that reasons over temporal specifications. The GFφ construction's exponential advantage is particularly relevant because repeated-reachability goals (GFφ) are the dominant specification pattern in RL benchmark suites.