AI Research Portal

This paper addresses the scalability challenge in stochastic planning problems in Markov Decision Processes (MDPs) with Linear Temporal Logic (LTL) goals. The core idea is to significantly reduce the state space of good-for-MDP (GFM) automata, which are used to represent LTL goals, through a sophisticated chain of transformations leveraging recent advances in good-for-games (GFG) minimisation. Additionally, the paper introduces a direct, provably single-exponential construction method for GFM automata for LTL formulas of the form GFφ, where φ is a co-safety formula. The main empirical claim is that the proposed state-reduction technique effectively reduces automata state space, and the specialized GFφ construction offers significant advantages in state size and runtime compared to standard GFM constructions.

Method

The paper proposes a state-space reduction technique for GFM automata and a direct construction for GFφ formulas.

GFM State Reduction Pipeline (Redux) The method employs a four-step chain of transformations to reduce the state space of an initial GFM automaton AGFM, yielding a 0/1-PA APA. The overall pipeline is LTL → LTL2GFM → AGFM → Redux → APA.

Step 1: GFM to DBA (Poly):
- The GFM automaton AGFM is transformed into a complete Deterministic Büchi Automaton (DBA) ADBA.
- This involves embedding the transition choices [k] (used in the product construction of MDPs and Büchi automata) into the transitions of AGFM.
- The MDP M is modified into M' by expanding its action set from Act to Act × [k].
- The automaton AGFM's transitions are re-labeled from Σ to Σ × [k], making ADBA deterministic.
- This step is polynomial in time.
Step 2: DBA to DCA (Const):
- The DBA ADBA is syntactically converted into a Deterministic Co-Büchi Automaton (DCA) ADCA.
- This is achieved by simply modifying the acceptance condition; ADCA has the same states, initial state, and transition function as ADBA.
- This step is done in constant runtime.
Step 3: GFG-Minimisation (Poly):
- A minimisation algorithm, originally developed for good-for-games (GFG) NCAs, is applied to ADCA.
- This yields a minimal GFG-NCA AGFG-Min.
- This step is polynomial in time.
Step 4: GFG-Min to 0/1-PA (Poly):
- The minimal GFG-NCA AGFG-Min is transformed into a language-equivalent 0/1-Probabilistic Automaton (PA) APA.
- This is done by resolving the nondeterminism with random choices, treating AGFG-Min as a Büchi automaton ANBA and building APA with QPA = QNBA, αPA = αNBA, and δPA(q, σ)(q') = 1 / |δNBA(q, σ)| for each q' ∈ δNBA(q, σ).
- This step is polynomial in time.

Direct GFM Construction for GFφ Formulas For LTL formulas of the form GFφ, where φ is a co-safety formula, a direct construction method is introduced.

An NFA Nφ = (Q, q0, δ, F) is first constructed for the co-safety property φ.
A GFM automaton A = (QA, qA, δA, αA) for GFφ is then constructed from Nφ.
- States: QA ⊆ ((Q \ F) ∪ {q0}), qA = q0.
- Transitions: For each q ∈ QA and σ ∈ Σ, δA(q, σ) is defined such that (1) q' ∈ δA(q, σ) if q' ∈ δ(q, σ) with q' ∉ F, and (2) q0 ∈ δA(q, σ).
- Acceptance Condition: αA = {(q, σ, q0) ∈ ∆(δA) | ∃q' ∈ δ(q, σ) ∧ q' ∈ F}.
This construction is provably single-exponential in the worst case.

Technical Details

Markov Decision Process (MDP): M = (S, Act, Σ, P, s0, L) where S is finite states, Act is actions, Σ is labels, P: S × Act × S → [0,1] is transition probability, s0 ∈ S is initial state, L: S × Act → Σ is labeling function.
LTL Formula: Defined as φ ::= a ∈ AP | ¬φ | φ∧φ | φ∨φ | Xφ | Gφ | Fφ | φUψ.
Automata:
- Nondeterministic Büchi Automaton (NBA): A = (Q, q0, δ, α) where Q is finite states, q0 is initial state, δ: Q × Σ → 2Q is transition function, α ⊆ ∆(δ) is accepting transitions.
- Good-for-MDP (GFM): An NBA A is GFM if for all finite MDPs M, Psem(M,A) = Psyn(M,A).
- 0/1-Probabilistic Automaton (PA): P = (Σ, Q, δ, q0, α) is a nondeterministic automaton with Büchi acceptance and a randomized transition function δ: Q × Σ ↔ Distr(Q). A 0/1-PA P has Pp(w) = 1 or Pp(w) = 0 for any word w.
Product MDP (M × A): For MDP M and NBA A, M × A = (S×, Act×, Σ, P×, (s0, q0), L×, α×) where S× = S × Q, Act× = Act × [k] (k is max out-degree of A), P×((s, q), (a, i), (s', q')) = P(s, a, s') if P(s, a, s') > 0 and q' ∈ δ(q, L(s, a)) where q' is the i-th state in ordered set δ(q, L(s, a)). L×((s, q), (a, i)) = L(s, a). α× = {((s,q), (a, i), (s', q')) | P×((s, q), (a, i), (s', q')) > 0, (q, L(s, a), q') ∈ α}.
Product MDP (M ⊗ P): For MDP M and 0/1-PA P, M ⊗ P = (S⊗, Act⊗, Σ, P⊗, (s0, q0), L⊗, α⊗) where S⊗ = S × Q, Act⊗ = Act, P⊗((s,q), a, (s', q')) = P(s, a, s') · δ(q, σ, q') if P(s, a, s') > 0 and σ = L(s, a). L⊗((s, q), a) = L(s, a). α⊗ = {((s,q), a, (s', q')) | (q, L(s,a), q') ∈ α, α ∈ Act⊗, P⊗((s, q), a, (s', q')) > 0}.
GFφ Construction Complexity: For a co-safety property φ, the NFA Nφ has 2O(|φ|) states. The GFM automaton A for GFφ constructed directly has 2O(|φ|) states. This is single-exponential, compared to 22O(|φ|) for general GFM constructions.
Implementation Details: Experiments used SPOT (Duret-Lutz 2013) for parts of patterns and GFG minimisation. LTL datasets from the Owl repository were used. All experiments ran on an 8-core ARM chip with 16GB of RAM.

Results

Datasets: LTL specifications from eight sources, including:
- Trigger with Delayed Response (TDR[n]): GF(a ∧ Xnb)
- Liberouter (LIB[n]): GF((a > X¬a) ∨ (¬a > Xa) ∨ (b ∧ X¬b) ∨ (¬b ∧ Xb) . . . )
- Bounded Retransmission Protocol (BRP[n]): G("msg_sent" → F("ack_send" ∧ σn))
- Etessami-Holzmann Patterns (EHP)
- Nested Until Dependencies (NU[n]): G(p1 → Okn)
- Layered Fairness and Reachability (LFR[n]): F(b1) ∧ (F(b2... F(bn)) ∧ GF(a1 ∧ X(a2 ∧ ...X(an))))
Metrics: Number of automata states, runtime (in seconds).
Baselines: Two state-of-the-art GFM constructions: Owl (Kretínský, Meggendorfer, and Sickert 2018) and Slim (Hahn et al. 2020). Reduced versions are denoted Owl-Red and Slim-Red.
Numeric Results (Table 1: GFM State Reduction):
- TDR[6]: Owl: 64 states (0.46s), Owl-Red: 64 states (0.03s), Slim: 65 states (0.09s), Slim-Red: 34 states (0.01s).
- TDR[7]: Owl: 128 states (0.46s), Owl-Red: 128 states (0.15s), Slim: 129 states (0.12s), Slim-Red: 66 states (0.02s).
- TDR[8]: Owl: 256 states (0.48s), Owl-Red: 256 states (0.69s), Slim: 257 states (0.14s), Slim-Red: 130 states (0.05s).
- LIB[4]: Owl: 17 states (0.44s), Owl-Red: 10 states (0.01s), Slim: 33 states (0.11s), Slim-Red: 18 states (0.13s).
- LIB[5]: Owl: 21 states (0.48s), Owl-Red: 12 states (0.01s), Slim: 65 states (0.20s), Slim-Red: 34 states (3.83s).
- LIB[6]: Owl: 25 states (0.62s), Owl-Red: 14 states (0.01s), Slim: 129 states (0.69s), Slim-Red: 66 states (128.34s).
- BRP[6]: Owl: 69 states (0.55s), Owl-Red: 17 states (0.02s), Slim: 317 states (0.14s), Slim-Red: 65 states (0.17s).
- BRP[7]: Owl: 133 states (0.65s), Owl-Red: 19 states (0.04s), Slim: 637 states (0.21s), Slim-Red: 95 states (0.71s).
- BRP[8]: Owl: 261 states (0.86s), Owl-Red: 21 states (0.14s), Slim: 1277 states (0.33s), Slim-Red: 146 states (3.49s).
- EHP: Owl: 13 states (0.43s), Owl-Red: 9 states (0.01s), Slim: 127 states (0.14s), Slim-Red: 54 states (0.31s).
- NU[4]: Owl: 44 states (1.16s), Owl-Red: 23 states (0.02s), Slim: 51 states (0.22s), Slim-Red: 39 states (0.02s).
- NU[5]: Owl: 150 states (1.41s), Owl-Red: 56 states (0.17s), Slim: 232 states (0.82s), Slim-Red: 159 states (0.76s).
- NU[6]: Owl: 433 states (5.92s), Owl-Red: 249 states (27.75s), Slim: 1425 states (12.24s), Slim-Red: 753 states (163.32s).
- LFR[6]: Owl: 39 states (0.77s), Owl-Red: 40 states (0.27s), Slim: 40 states (0.44s), Slim-Red: 21 states (0.19s).
- LFR[7]: Owl: 72 states (0.92s), Owl-Red: 73 states (2.99s), Slim: 73 states (1.57s), Slim-Red: 34 states (1.76s).
- LFR[8]: Owl: 137 states (1.45s), Owl-Red: 138 states (39.11s), Slim: 138 states (10.74s), Slim-Red: 59 states (20.84s).
Numeric Results (Table 2: Direct GFM-GF Construction):
- TDR[6]: Owl-Red: 64 states (0.49s), Slim-Red: 34 states (0.10s), GFM-GF: 7 states (0.08s).
- TDR[7]: Owl-Red: 128 states (0.61s), Slim-Red: 66 states (0.14s), GFM-GF: 8 states (0.08s).
- TDR[8]: Owl-Red: 256 states (1.17s), Slim-Red: 130 states (0.19s), GFM-GF: 9 states (0.08s).
- TDR[9]: Owl-Red: 512 states (4.27s), Slim-Red: 258 states (0.48s), GFM-GF: 10 states (0.10s).
- TDR[10]: Owl-Red: 1024 states (23.67s), Slim-Red: 514 states (0.91s), GFM-GF: 11 states (0.09s).
- LIB[6]: Owl-Red: 14 states (0.63s), Slim-Red: 66 states (129.03s), GFM-GF: 13 states (0.09s).
- LIB[7]: Owl-Red: 16 states (1.47s), Slim-Red: timeout, GFM-GF: 15 states (0.12s).
- LIB[8]: Owl-Red: 18 states (5.95s), Slim-Red: timeout, GFM-GF: 17 states (0.20s).
- LIB[9]: Owl-Red: 20 states (37.78s), Slim-Red: timeout, GFM-GF: 19 states (0.23s).
Runtime/Training Cost: Timeout for experiments is 300 seconds. For LFR, Owl returns incomplete automata, while the reduction returns complete ones. For LIB[7], LIB[8], and LIB[9], Slim-Red timed out during reduction. For LIB[7], LIB[8], and LIB[9], Owl-Red and Slim-Red timed out during automata construction when compared to GFM-GF.

Good-for-MDP State Reduction for Stochastic LTL Planning

Summary

Problem

Key Contributions

Method

Technical Details

Results

Weaknesses / Limitations

Evidence

Additional Figures