跳转至

Good-for-MDP State Reduction for Stochastic LTL Planning

会议: AAAI 2026
arXiv: 2511.09073
代码: 无
领域: 强化学习
关键词: LTL规划, 马尔可夫决策过程, 自动机状态约简, Good-for-MDP, 形式化方法

一句话总结

提出一种新的 Good-for-MDP（GFM）自动机状态约简技术，通过 GFM→DBA→DCA→GFG 最小化→0/1-PA 的变换链显著减少自动机状态数量；同时为 \(\textsf{GF}\varphi\)（\(\varphi\) 为 co-safety 公式）类公式提供直接的单指数构造方法，相比一般的双指数构造实现了指数级的状态数减少。

研究背景与动机

LTL 时序逻辑规划的核心管道：在随机规划问题中，将环境建模为马尔可夫决策过程（MDP）\(\mathcal{M}\)，任务目标用线性时序逻辑（LTL）公式 \(\varphi\) 描述。核心求解流程为： 1. 将 LTL 公式转化为自动机 \(\mathcal{A}\) 2. 构建乘积 MDP \(\mathcal{M} \times \mathcal{A}\) 3. 在乘积 MDP 中识别接受端组件（accepting MECs），求解最大化到达概率的策略

GFM 自动机的地位： - 确定性自动机（DRA）：可直接用于乘积构造，但从 LTL 构造 DRA 涉及 Safra 构造等复杂技术 - GFM 自动机：一种受限的非确定性 Büchi 自动机（NBA），其非确定性可以由智能体在策略综合时解析，不影响最优满足概率。实践中比 DRA 小得多，是当前最先进方法（PRISM 等）的核心组件

核心瓶颈——自动机大小：影响整个规划方法可扩展性的最大因素是 GFM 自动机的状态数量。状态越多，乘积 MDP 越大，策略综合越慢。

研究目标： 1. 提出通用的 GFM 状态空间约简技术 2. 对常见的 \(\textsf{GF}\varphi\) 类公式，提供更高效的直接构造方法

方法详解

整体框架

状态约简管道分为四步（见 Figure 1）：

\[\mathcal{A}_\text{GFM} \xrightarrow{\text{Poly}} \mathcal{A}_\text{DBA} \xrightarrow{\text{Const}} \mathcal{A}_\text{DCA} \xrightarrow{\text{Poly}} \mathcal{A}_\text{GFG-Min} \xrightarrow{\text{Poly}} \mathcal{A}_\text{PA}\]

所有步骤均为多项式或常数时间。

关键设计

1. Step 1: GFM→DBA（将非确定性编码到 MDP 动作中）

核心思路：GFM 自动机的非确定性可由智能体解析——将非确定性选择 \([k]\) 编码进 MDP 的动作空间，使自动机变为确定性的。

  • 修改 MDP：动作空间从 \(\text{Act}\) 扩展为 \(\text{Act} \times [k]\)，标签空间从 \(\Sigma\) 扩展为 \(\Sigma \times [k]\)
  • 修改自动机：转移函数在扩展字母表上变为确定性：\(\delta_\text{DBA}(q, \langle\sigma, i\rangle) = q'\)，其中 \(q'\) 是 \(\delta(q,\sigma)\) 中第 \(i\) 个状态

关键引理（Lemma 1）：乘积 \(\mathcal{M} \times \mathcal{A}_\text{GFM}\) 与 \(\mathcal{M}' \times \mathcal{A}_\text{DBA}\) 完全相同（状态空间一致，最优策略等价）。

设计动机：后续的 GFG 最小化技术需要确定性或 GFG 的输入自动机。将 GFM 的非确定性"外包"给 MDP 动作后，自动机变为确定性的，为最小化创造条件。

2. Step 2-3: DBA→DCA→GFG 最小化

Step 2（常数时间）：将 DBA 的接受条件（\(\alpha\)）重解释为 DCA 的拒绝条件——语言取补，但状态转移结构不变。这是一个纯语义操作。

Step 3（多项式时间）：应用 Radi & Kupferman (2022) 的 GFG co-Büchi 自动机最小化算法。关键在于： - DCA 是确定性的，因此也是 GFG 的 - GFG co-Büchi 自动机可在多项式时间内最小化 - 最小化输出一个最小 GFG-NCA \(\mathcal{A}_\text{GFG-Min}\)

为什么可以跨范式使用 GFG 最小化：GFG 自动机（用于对抗性博弈）的最小化技术之前未被用于 MDP 设置。本文的关键贡献是建立了 GFM（概率设置）与 GFG（对抗设置）之间的桥梁——通过 DBA 中间表示连接两者。

3. Step 4: GFG-Min→0/1-PA（概率自动机）

核心思路：Li et al. (2025) 证明了最小 GFG-NCA 可通过均匀随机化非确定性转换为语言等价的 0/1-PA：

\[\delta_\text{PA}(q,\sigma)(q') = \frac{1}{|\delta_\text{NBA}(q,\sigma)|}\]

0/1-PA 的 GFM 性质（Theorem 2，本文新贡献）：首次证明 0/1-PA 可作为另一种 GFM 自动机使用。关键区别：在乘积 MDP \(\mathcal{M}' \otimes \mathcal{A}_\text{PA}\) 中，后继状态选择由随机策略决定（而非智能体选择），因此动作空间仅为 \(\text{Act}\)（无需 \([k]\)），乘积更小。

主定理（Theorem 4）：从 \(\mathcal{M}' \otimes \mathcal{A}_\text{PA}\) 上的最优策略可提取原问题 \(\mathcal{M}\) 的最优策略，实现 \(\text{Psem}(\mathcal{M}, \mathcal{A}_\text{GFM})\)。

4. \(\textsf{GF}\varphi\) 的直接单指数构造（Section 6）

\(\textsf{GF}\varphi\)（\(\varphi\) 为 co-safety 公式）表达"有限模式无限次重复"的重复可达属性，常见于验证和强化学习。

构造方法：从 \(\varphi\) 对应的 NFA \(\mathcal{N}_\varphi = (Q, q_0, \delta, F)\) 构造 GFM 自动机 \(\mathcal{A}\)： - 状态空间：\(Q_\mathcal{A} \subseteq (Q \setminus F) \cup \{q_0\}\)（去掉终态，保留初态） - 转移规则：(1) 非终态后继保留；(2) 任何状态都可以重置到 \(q_0\) - 接受条件：当某转移到达 \(q_0\) 且在 NFA 中对应到达终态时，标记为接受转移

直觉：对于 \(\textsf{GF}\varphi\)，可以在任意时刻"忘记"过去的有限轨迹，重新开始追踪 \(\varphi\) 是否被满足。Büchi 条件确保 \(\varphi\) 被无限次满足。

Theorem 5：\(\mathcal{A}\) 识别 \([\textsf{GF}\varphi]\)，是 GFM 的，且仅有 \(2^{\mathcal{O}(|\varphi|)}\) 个状态——相比一般构造的 \(2^{2^{\mathcal{O}(|\varphi|)}}\) 实现了指数级改进。

损失函数 / 训练策略

本文不涉及学习/训练。最终策略综合通过标准的 MDP 可达性分析：在乘积 MDP 中识别包含接受转移的 MEC，计算最大化到达这些 MEC 概率的无记忆策略。

实验关键数据

主实验

GFM 状态约简效果——6 类 LTL 模式对比（Table 1），报告自动机状态数/运行时间：

模式 Owl Owl-Red Slim Slim-Red
TDR[6] 64 (0.46s) 64 (0.03s) 65 (0.09s) 34 (0.01s)
TDR[8] 256 (0.48s) 256 (0.69s) 257 (0.14s) 130 (0.05s)
BRP[6] 69 (0.55s) 17 (0.02s) 317 (0.14s) 65 (0.17s)
BRP[8] 261 (0.86s) 21 (0.14s) 1277 (0.33s) 146 (3.49s)
EHP 13 (0.43s) 9 (0.01s) 127 (0.14s) 54 (0.31s)
NU[5] 150 (1.41s) 56 (0.17s) 232 (0.82s) 159 (0.76s)
LFR[7] 72 (0.92s) 73 (2.99s) 73 (1.57s) 34 (1.76s)

消融实验

\(\textsf{GF}\varphi\) 直接构造 vs 最先进约简方法（Table 2）：

模式 Owl-Red（含构造） Slim-Red（含构造） GFM-GF（直接构造）
TDR[6] 64 (0.49s) 34 (0.10s) 7 (0.08s)
TDR[8] 256 (1.17s) 130 (0.19s) 9 (0.08s)
TDR[10] 1024 (23.67s) 514 (0.91s) 11 (0.09s)
LIB[6] 14 (0.63s) 66 (129s) 13 (0.09s)
LIB[8] 18 (5.95s) timeout 17 (0.20s)
LIB[9] 20 (37.78s) timeout 19 (0.23s)

关键发现

  1. 约简后的自动机在所有模式中都是最小的（Table 1 加粗值），且约简本身开销低（通常 <1s）
  2. BRP 模式约简最显著：BRP[8] 从 261 状态降至 21 状态（约简 12.4 倍），因为该模式中大量转移是冗余的
  3. \(\textsf{GF}\varphi\) 直接构造实现指数级改进：TDR[10] 从 Owl-Red 的 1024 状态降至 GFM-GF 的仅 11 状态——线性 vs 指数增长
  4. 时间优势同样显著：TDR[10] Owl-Red 需 23.67s，GFM-GF 仅需 0.09s——加速 260 倍
  5. Slim 构造因缺乏优化，约简提升更大：Slim-Red 跌幅大于 Owl-Red，因为 Owl 自身已有高级公式简化
  6. LIB 模式 Slim-Red 超时：GFG 最小化在某些复杂模式上耗时较长（LIB[6] 128s），而直接构造仍在 0.2s 内

亮点与洞察

  1. 跨范式的技术桥接：将 GFG 最小化（对抗博弈理论）引入 GFM 设置（概率规划），通过 DBA/DCA 中间表示实现了看似不相关领域的技术迁移
  2. 0/1-PA 作为新型 GFM 自动机：首次证明概率自动机可在 MDP 中替代 GFM 使用——非确定性由随机化解析而非智能体解析——这意味着乘积 MDP 的动作空间更小
  3. 理论与实践并重：不仅有严格的正确性证明链（Theorem 2→3→4），还有覆盖 8+ 文献来源的全面基准实验
  4. \(\textsf{GF}\varphi\) 构造的优雅直觉：重复可达属性可通过"随时重置到初态"的简单策略处理——Büchi 条件自然保证无限次满足

局限与展望

  1. GFG 最小化本身可能耗时：在 NU[6]（27.75s）、LFR[8]（39.11s）等复杂模式上约简时间不可忽略
  2. 仅限 Büchi/co-Büchi 条件：Rabin 条件的 GFM 约简未在实验中验证（论文提及可推广但未实现）
  3. 未集成到主流工具：PRISM、Owl 等工具尚未内置本文的约简管道
  4. \(\textsf{GF}\varphi\) 构造限于 co-safety 子公式：完整 LTL 仍需双指数构造
  5. 缺少端到端规划实验：仅报告自动机状态数/时间，未展示对最终 MDP 策略综合性能的影响
  6. 在线求解器的集成：约简后的自动机如何与在线 POMDP 求解器协同未探讨

相关工作与启发

  • LTL-to-GFM：Sickert et al. 2016（"slim"构造）、Hahn et al. 2020（GFM 形式化定义）→ 本文在其输出上进一步约简
  • GFG 最小化：Radi & Kupferman 2022 → 本文将其从对抗设置迁移到概率设置
  • 0/1-PA 理论：Li et al. 2025（语义确定性证明）→ 本文证明其 GFM 性质
  • 强化学习中的 LTL：Jackermeier & Abate 2025 使用 \(\textsf{GF}\varphi\) → 本文的直接构造可直接加速
  • 可启发 RL 中自动机表示的自动压缩和效率优化

评分

  • 新颖性: ⭐⭐⭐⭐⭐ — GFM-GFG 桥接和 0/1-PA 的 GFM 性质均为首创理论贡献
  • 实验充分度: ⭐⭐⭐⭐ — 覆盖 6 类模式 8+ 来源的全面基准，但缺少端到端规划实验
  • 写作质量: ⭐⭐⭐⭐ — 变换管道清晰，但形式化定义密度高，需要自动机理论背景
  • 价值: ⭐⭐⭐⭐⭐ — 对 LTL 规划、概率验证、RL 均有直接影响的基础性贡献

相关论文