假设你负责一个无人小车的任务规划模块。小车在仓库里执行搬运任务需要满足一个很常见的规格反复经过充电区同时永远避开高危区域。你把这个规格写成线性时序逻辑公式然后用马尔可夫决策过程MDP做策略合成。结果一测成功率很漂亮0.98。但换一个测试环境成功率立刻掉到 0.83。问题出在哪问题几乎总是出在转移概率上。仿真环境里的转移概率是估计值不是真值把估计值当成精确值去求解 MDP得到的 0.98 只是“名义概率”不是系统真正能达到的保障。鲁棒 MDPRobust MDP就是为这种不确定性设计的建模框架而 ω-regular 目标则是表达“反复发生”“最终避免”“永远安全”这类长期性质的规格语言。把两者结合做定量分析Quantitative Analysis回答的是更硬核的问题在环境参数最坏情况下策略能以多大的概率满足规格这篇博客从一个判断开始鲁棒 MDP 的定量分析不是普通 MDP 分析加一个“误差棒”而是把 min-max 语义直接放进值迭代、策略迭代和自动机乘积的每一步。读完这篇文章你会理解鲁棒贝尔曼算子为什么是这样设计的、ω-regular 目标如何转成自动机乘积、以及一个可运行的鲁棒值迭代最小示例长什么样。文章也会把新手最容易踩的坑比如区间不确定性下内层 min 算错、Büchi 目标下值迭代不收敛、非矩形不确定性导致 NP-hard 等问题逐个讲清楚。1. 这篇文章真正要解决的问题先看三个真实痛点。第一个痛点是转移概率不可靠。传统 MDP 的定量分析假设转移矩阵 P(s,a,·) 是精确已知的。实际工程里这个矩阵通常从有限样本里估计出来样本量不够、环境漂移、对手干预都会让真实概率偏离估计值。于是“最优策略”可能只在名义模型上最优。第二个痛点是规格往往是长期性质。很多任务不能只用“一步奖励最大”或“有限步内到达目标”来表达。比如网络协议要求“无限次重传最终成功”、机器人任务要求“永远不进入危险区域且经常充电”、缓存策略要求“缓存命中率长期维持在上限”。这些规格对应的正是 ω-regular 语言典型代表是线性时序逻辑LTL中的GF goal、FG safe、parity 条件等。第三个痛点是“能不能满足”不够用还要知道“有多大把握”。定性分析回答的是是否存在一个策略使得规格以概率 1 满足即 almost-sure winning。但现实中很多系统做不到概率 1我们想知道最优策略下能满足的最坏情况概率是多少、安全裕度有多大、在区间边界下策略是否仍然可用。这就是定量分析的价值。这篇文章适合以下读者做强化学习但发现仿真到真实环境有 gap 的同学做机器人任务规划、网络协议验证、可靠性工程的工程师以及形式化方法方向刚入门、想弄懂鲁棒 MDP 到底在做什么的研究者。判断标准很简单如果你关心“策略在真实环境中最坏能有多好”而不是“在仿真模型里有多好”那么鲁棒 MDP 的定量分析就是你需要补的一课。2. 基础概念与核心原理MDP、ω-regular 目标与鲁棒 MDP2.1 普通 MDP 与策略马尔可夫决策过程通常写成四元组 (S, A, P, r)。S 是状态集合A 是动作集合P(s,a,·) 是在状态 s 执行动作 a 后的转移概率分布r(s,a) 是即时奖励或代价。策略 π 决定每个状态下选哪个动作。给定一个策略系统在状态空间上形成一条无限随机轨迹。普通 MDP 的定量分析有两种典型问题一是“给定策略满足某个性质的概率是多少”二是“在所有策略中最大化这个概率的最优值是多少”。前者是策略评估后者是策略合成。经典算法包括值迭代、策略迭代、线性规划。2.2 ω-regular 目标与 ω-自动机ω-regular 语言是定义在无限轨迹上的正则语言能表达“无限执行过程中反复出现的条件”。最常见的子类包括目标类型典型 LTL 写法直观含义接受条件可达性F goal最终到达目标轨迹上某点满足 goal安全性G safe永远安全轨迹上每点都满足 safeBüchiG F goal无限次满足 goal接受状态被访问无限次co-BüchiF G safe最终永远安全拒绝状态只被访问有限次Parity由自动机给出最大颜色出现无限次且为偶奇偶条件为什么要引入自动机因为计算机不擅长直接处理 LTL 公式但非常擅长处理有限自动机。把 ω-regular 规格转成确定性奇偶自动机DPA或确定性 Rabin 自动机后原本要一路看到底的无限轨迹性质就变成在自动机状态上的接受条件。这是模型检验和策略合成中最关键的一步。2.3 鲁棒 MDP 的建模假设鲁棒 MDP 与普通 MDP 的唯一区别在于转移概率不再是一个固定分布而是一个不确定集合 U(s,a)。每个状态动作对都对应一个候选概率分布集合系统实际运行时的真实分布未知但保证落在这个集合内。最常用的是矩形不确定集合rectangular uncertainty setU(s,a) { p ∈ Δ(S) : l(s,a,s) ≤ p(s,a,s) ≤ u(s,a,s) }其中 l 和 u 分别是转移概率的下界和上界。矩形性表示每个状态动作对的不确定性可以独立选取不会跨状态跨动作耦合。这个假设非常重要后面会专门解释。除了区间集合工程中还常用 L1 球、L∞ 球、KL 散度球等。它们通常由一个名义分布和一个半径参数定义例如U(s,a) { p : D_KL(p || p̂(s,a)) ≤ ε }这类集合的好处是能从统计置信区间自然地构造出来。一个容易混淆的点是鲁棒 MDP 不是“带随机初始状态”的 MDP也不是“参数服从某个先验分布”的贝叶斯 MDP。在鲁棒 MDP 里真实转移概率是未知但固定的我们考虑的是最坏情况而不是平均情况。这是频率派与贝叶斯派思路在决策问题上的一个典型分叉。3. 核心算法鲁棒贝尔曼算子与 minimax 求解3.1 鲁棒贝尔曼算子普通 MDP 的贝尔曼最优算子写作(Tv)(s) max_{a∈A} [ r(s,a) γ Σ_{s} P(s,a,s) v(s) ]鲁棒 MDP 的核心变化是因为转移概率不确定内层不再是一个固定的期望值而是要在不确定集合里求最小期望。于是算子变成(Tv)(s) max_{a∈A} min_{p∈U(s,a)} [ r(s,a) γ Σ_{s} p(s) v(s) ]这个形式就是典型的 minimax 结构外层最大化策略收益内层最小化环境参数。它表达了“最坏情况下的最优值”也是鲁棒动态规划的基本出发点。这种变化带来两个直接后果。第一值迭代的每一步都要解一个内层优化问题计算成本比普通 MDP 高。第二贝尔曼算子是否仍然是压缩映射、是否保持单调性取决于不确定集合的形状和问题设置。对折扣情形只要不确定集合是紧的凸集鲁棒贝尔曼算子仍然可以做值迭代对无折扣的 reachability 或 Büchi 目标情况更复杂后面会讲到。3.2 内层 min 问题如何高效求解内层问题本质上是min_{p ∈ U(s,a)} Σ_{s} p(s) v(s)这是一个关于 p 的线性目标函数。不同形状的 U 对应不同的算法区间集合可以用贪心算法。把状态按 v(s) 从小到大排序先给下界再把剩余概率优先分配给 v 最小的状态直到上界或概率总和用完。L1 球本质上是线性规划但有闭式解可以通过排序后的分位数直接求解。L∞ 球因为每个坐标都有独立上下界通常比 L1 更容易直接做坐标级 min 即可。KL 散度球内层是一个带 KL 约束的期望最小化可以通过拉格朗日对偶化为一个标量方程用二分法求对偶变量。从工程角度看最稳妥的实现方式是先把不确定集合转成线性约束然后用成熟的线性规划库如 scipy.optimize.linprog验证贪心或闭式解的正确性。生产代码里再用解析解替换 LP以控制性能。3.3 矩形性为什么重要如果不确定集合不是矩形的即不同状态动作对之间的概率扰动存在耦合那么整体问题可能变成 NP-hard。原因是耦合会让问题变成一个联立的非凸优化很难分解到单个状态动作对去求解。矩形性保证了“每个状态动作对独立最坏化”是全局最优策略评估的正确方式也让动态规划可以逐点进行。所以读者在看到一篇论文说“我们求解一般鲁棒 MDP”时第一反应应该看它的不确定集合是不是矩形。如果不是它要么用了近似算法要么问题规模非常小要么做了一些额外假设。这是鲁棒 MDP 领域最容易误读的地方之一。4. ω-regular 目标的产品自动机构造4.1 从 LTL 到确定性奇偶自动机处理 ω-regular 目标的标准路线是LTL 公式 → 确定性奇偶自动机DPA → 与 MDP 做乘积 → 在乘积 MDP 上求解定量问题为什么要确定性自动机因为 MDP 的策略需要根据当前状态做决策如果自动机是非确定的策略不知道“当前实际处于自动机的哪个状态”语义会复杂化。确定性 Büchi 自动机并不能接受所有 ω-regular 语言所以实践中常用确定性奇偶自动机或确定性 Rabin 自动机。工具方面Spot 的ltl2tgba、Owl、ltl2dstar、Rabinizer 都可以完成这类转换。4.2 构建乘积 MDP设 MDP 的状态为 s自动机的状态为 q。乘积状态是 (s,q)。每执行一个动作 aMDP 转移到 s同时根据 s 满足的原子命题集合更新自动机状态 q δ(q, L(s))。乘积 MDP 的转移概率继承原始 MDP 的转移概率。对于一个 LTL 公式 φ原问题“MDP 中满足 φ 的最优概率”就等价于“乘积 MDP 中满足自动机接受条件的最优概率”。对于 parity 条件接受语义变成轨迹上无限次出现的最大颜色编号是偶数。这个转换是精确的没有信息损失。4.3 端部组件与接受条件问题到这一步还没有完全解决。对于 Büchi、parity 这类长期目标值迭代如果直接套用折扣奖励的算法往往不收敛或收敛到错误值。原因是状态空间中存在端部组件end componentEC即一组状态在某个策略下可以无限保持在其中且概率质量不再离开。为了正确计算长期目标的概率必须先找出极大端部组件MEC并把接受条件映射到端部组件上一个端部组件是“接受”的当且仅当它包含接受条件对应的状态。在鲁棒 MDP 中端部组件的处理还要额外小心。因为转移概率是不确定的某个端部组件是否“几乎必然可达”取决于最坏情况下的概率下界而不是名义概率。也就是说原本在普通 MDP 里一个简单的图论可达性判断在鲁棒 MDP 里需要结合区间概率重新分析。5. 工具链与环境准备5.1 推荐工具工具定位适用场景PRISM经典概率模型检验器普通 MDP、LTL/概率 CTL 性质验证算法正确性Storm高性能概率模型检验器大规模 MDP、部分版本支持鲁棒模型检验C 与 Python 绑定SpotLTL 与 ω-自动机库LTL 转自动机、自动机化简、DPA 构造Owl / ltl2dstar / Rabinizer自动机转换工具生成确定性 Rabin/parity 自动机自研 Python算法原型验证理解算法、小规模实验、定制鲁棒集合5.2 运行环境建议使用 Linux 或 WSL2。Python 环境建议 3.8 以上安装以下依赖即可跑通本文示例pip install numpy scipy spotPRISM 需要从官网下载对应平台的压缩包不同操作系统安装方式不同这里不做版本写死以官方安装文档为准。Storm 推荐用官方 Docker 镜像或者按 GitHub 仓库的构建说明编译Python 绑定也可以从源码构建。版本细节不展开是因为这些工具迭代较快写死版本对读者反而没有意义。6. 完整示例与代码实现6.1 示例问题带区间不确定性的三状态鲁棒 MDP我们构造一个最小但完整的例子。状态 0 是起点状态 1 是目标吸收态状态 2 是失败吸收态。在状态 0 有两个动作动作 a到达目标概率在 [0.7, 0.8]失败概率在 [0.1, 0.2]留在原地的概率在 [0, 0.2]。动作 b到达目标概率在 [0.5, 0.6]留在原地的概率在 [0.2, 0.4]失败概率在 [0, 0.3]。目标是最小化最坏情况下到达目标状态的概率。这个例子的好处是可以用手算验证设 v0 为状态 0 的鲁棒值v11v20。动作 a 的最坏概率会尽可能把质量分给失败态和起点得到 v 0.7 0.1×v0动作 b 得到 v 0.5 0.2×v0。比较后动作 a 更优解方程 v0 0.7 0.1×v0得到 v0 0.7778。6.2 代码一鲁棒值迭代实现下面是一份完整可运行的 Python 实现重点在inner_min_expectation函数它用贪心算法求解区间集合下的内层最小期望。# file: robust_mdp_example.py import numpy as np def inner_min_expectation(lo, hi, v): 求解 min_{p: lo p hi, sum(p)1} p v 区间 单纯形约束下贪心分配即可得到最优解。 思路概率先按下界放置剩余质量优先分配给 v 最小的状态。 n len(v) p lo.copy() remaining 1.0 - p.sum() for i in sorted(range(n), keylambda idx: v[idx]): if remaining 1e-12: break add min(hi[i] - lo[i], remaining) p[i] add remaining - add return float(p v), p def robust_value_iteration(states, actions, lo, hi, eps1e-8, max_iter10000): # 状态 1 是目标吸收态值固定为 1状态 2 是失败吸收态值固定为 0 v np.zeros(len(states)) v[1] 1.0 transient [s for s in states if actions[s]] for it in range(max_iter): v_new v.copy() for s in transient: best -np.inf for a in actions[s]: e, _ inner_min_expectation(lo[s][a], hi[s][a], v) best max(best, e) v_new[s] best diff np.max(np.abs(v_new - v)) v v_new if diff eps: return v, it 1 return v, max_iter states [0, 1, 2] actions {0: [0, 1], 1: [], 2: 鲁棒MDP定量分析：不确定性下的ω-regular目标策略合成
假设你负责一个无人小车的任务规划模块。小车在仓库里执行搬运任务需要满足一个很常见的规格反复经过充电区同时永远避开高危区域。你把这个规格写成线性时序逻辑公式然后用马尔可夫决策过程MDP做策略合成。结果一测成功率很漂亮0.98。但换一个测试环境成功率立刻掉到 0.83。问题出在哪问题几乎总是出在转移概率上。仿真环境里的转移概率是估计值不是真值把估计值当成精确值去求解 MDP得到的 0.98 只是“名义概率”不是系统真正能达到的保障。鲁棒 MDPRobust MDP就是为这种不确定性设计的建模框架而 ω-regular 目标则是表达“反复发生”“最终避免”“永远安全”这类长期性质的规格语言。把两者结合做定量分析Quantitative Analysis回答的是更硬核的问题在环境参数最坏情况下策略能以多大的概率满足规格这篇博客从一个判断开始鲁棒 MDP 的定量分析不是普通 MDP 分析加一个“误差棒”而是把 min-max 语义直接放进值迭代、策略迭代和自动机乘积的每一步。读完这篇文章你会理解鲁棒贝尔曼算子为什么是这样设计的、ω-regular 目标如何转成自动机乘积、以及一个可运行的鲁棒值迭代最小示例长什么样。文章也会把新手最容易踩的坑比如区间不确定性下内层 min 算错、Büchi 目标下值迭代不收敛、非矩形不确定性导致 NP-hard 等问题逐个讲清楚。1. 这篇文章真正要解决的问题先看三个真实痛点。第一个痛点是转移概率不可靠。传统 MDP 的定量分析假设转移矩阵 P(s,a,·) 是精确已知的。实际工程里这个矩阵通常从有限样本里估计出来样本量不够、环境漂移、对手干预都会让真实概率偏离估计值。于是“最优策略”可能只在名义模型上最优。第二个痛点是规格往往是长期性质。很多任务不能只用“一步奖励最大”或“有限步内到达目标”来表达。比如网络协议要求“无限次重传最终成功”、机器人任务要求“永远不进入危险区域且经常充电”、缓存策略要求“缓存命中率长期维持在上限”。这些规格对应的正是 ω-regular 语言典型代表是线性时序逻辑LTL中的GF goal、FG safe、parity 条件等。第三个痛点是“能不能满足”不够用还要知道“有多大把握”。定性分析回答的是是否存在一个策略使得规格以概率 1 满足即 almost-sure winning。但现实中很多系统做不到概率 1我们想知道最优策略下能满足的最坏情况概率是多少、安全裕度有多大、在区间边界下策略是否仍然可用。这就是定量分析的价值。这篇文章适合以下读者做强化学习但发现仿真到真实环境有 gap 的同学做机器人任务规划、网络协议验证、可靠性工程的工程师以及形式化方法方向刚入门、想弄懂鲁棒 MDP 到底在做什么的研究者。判断标准很简单如果你关心“策略在真实环境中最坏能有多好”而不是“在仿真模型里有多好”那么鲁棒 MDP 的定量分析就是你需要补的一课。2. 基础概念与核心原理MDP、ω-regular 目标与鲁棒 MDP2.1 普通 MDP 与策略马尔可夫决策过程通常写成四元组 (S, A, P, r)。S 是状态集合A 是动作集合P(s,a,·) 是在状态 s 执行动作 a 后的转移概率分布r(s,a) 是即时奖励或代价。策略 π 决定每个状态下选哪个动作。给定一个策略系统在状态空间上形成一条无限随机轨迹。普通 MDP 的定量分析有两种典型问题一是“给定策略满足某个性质的概率是多少”二是“在所有策略中最大化这个概率的最优值是多少”。前者是策略评估后者是策略合成。经典算法包括值迭代、策略迭代、线性规划。2.2 ω-regular 目标与 ω-自动机ω-regular 语言是定义在无限轨迹上的正则语言能表达“无限执行过程中反复出现的条件”。最常见的子类包括目标类型典型 LTL 写法直观含义接受条件可达性F goal最终到达目标轨迹上某点满足 goal安全性G safe永远安全轨迹上每点都满足 safeBüchiG F goal无限次满足 goal接受状态被访问无限次co-BüchiF G safe最终永远安全拒绝状态只被访问有限次Parity由自动机给出最大颜色出现无限次且为偶奇偶条件为什么要引入自动机因为计算机不擅长直接处理 LTL 公式但非常擅长处理有限自动机。把 ω-regular 规格转成确定性奇偶自动机DPA或确定性 Rabin 自动机后原本要一路看到底的无限轨迹性质就变成在自动机状态上的接受条件。这是模型检验和策略合成中最关键的一步。2.3 鲁棒 MDP 的建模假设鲁棒 MDP 与普通 MDP 的唯一区别在于转移概率不再是一个固定分布而是一个不确定集合 U(s,a)。每个状态动作对都对应一个候选概率分布集合系统实际运行时的真实分布未知但保证落在这个集合内。最常用的是矩形不确定集合rectangular uncertainty setU(s,a) { p ∈ Δ(S) : l(s,a,s) ≤ p(s,a,s) ≤ u(s,a,s) }其中 l 和 u 分别是转移概率的下界和上界。矩形性表示每个状态动作对的不确定性可以独立选取不会跨状态跨动作耦合。这个假设非常重要后面会专门解释。除了区间集合工程中还常用 L1 球、L∞ 球、KL 散度球等。它们通常由一个名义分布和一个半径参数定义例如U(s,a) { p : D_KL(p || p̂(s,a)) ≤ ε }这类集合的好处是能从统计置信区间自然地构造出来。一个容易混淆的点是鲁棒 MDP 不是“带随机初始状态”的 MDP也不是“参数服从某个先验分布”的贝叶斯 MDP。在鲁棒 MDP 里真实转移概率是未知但固定的我们考虑的是最坏情况而不是平均情况。这是频率派与贝叶斯派思路在决策问题上的一个典型分叉。3. 核心算法鲁棒贝尔曼算子与 minimax 求解3.1 鲁棒贝尔曼算子普通 MDP 的贝尔曼最优算子写作(Tv)(s) max_{a∈A} [ r(s,a) γ Σ_{s} P(s,a,s) v(s) ]鲁棒 MDP 的核心变化是因为转移概率不确定内层不再是一个固定的期望值而是要在不确定集合里求最小期望。于是算子变成(Tv)(s) max_{a∈A} min_{p∈U(s,a)} [ r(s,a) γ Σ_{s} p(s) v(s) ]这个形式就是典型的 minimax 结构外层最大化策略收益内层最小化环境参数。它表达了“最坏情况下的最优值”也是鲁棒动态规划的基本出发点。这种变化带来两个直接后果。第一值迭代的每一步都要解一个内层优化问题计算成本比普通 MDP 高。第二贝尔曼算子是否仍然是压缩映射、是否保持单调性取决于不确定集合的形状和问题设置。对折扣情形只要不确定集合是紧的凸集鲁棒贝尔曼算子仍然可以做值迭代对无折扣的 reachability 或 Büchi 目标情况更复杂后面会讲到。3.2 内层 min 问题如何高效求解内层问题本质上是min_{p ∈ U(s,a)} Σ_{s} p(s) v(s)这是一个关于 p 的线性目标函数。不同形状的 U 对应不同的算法区间集合可以用贪心算法。把状态按 v(s) 从小到大排序先给下界再把剩余概率优先分配给 v 最小的状态直到上界或概率总和用完。L1 球本质上是线性规划但有闭式解可以通过排序后的分位数直接求解。L∞ 球因为每个坐标都有独立上下界通常比 L1 更容易直接做坐标级 min 即可。KL 散度球内层是一个带 KL 约束的期望最小化可以通过拉格朗日对偶化为一个标量方程用二分法求对偶变量。从工程角度看最稳妥的实现方式是先把不确定集合转成线性约束然后用成熟的线性规划库如 scipy.optimize.linprog验证贪心或闭式解的正确性。生产代码里再用解析解替换 LP以控制性能。3.3 矩形性为什么重要如果不确定集合不是矩形的即不同状态动作对之间的概率扰动存在耦合那么整体问题可能变成 NP-hard。原因是耦合会让问题变成一个联立的非凸优化很难分解到单个状态动作对去求解。矩形性保证了“每个状态动作对独立最坏化”是全局最优策略评估的正确方式也让动态规划可以逐点进行。所以读者在看到一篇论文说“我们求解一般鲁棒 MDP”时第一反应应该看它的不确定集合是不是矩形。如果不是它要么用了近似算法要么问题规模非常小要么做了一些额外假设。这是鲁棒 MDP 领域最容易误读的地方之一。4. ω-regular 目标的产品自动机构造4.1 从 LTL 到确定性奇偶自动机处理 ω-regular 目标的标准路线是LTL 公式 → 确定性奇偶自动机DPA → 与 MDP 做乘积 → 在乘积 MDP 上求解定量问题为什么要确定性自动机因为 MDP 的策略需要根据当前状态做决策如果自动机是非确定的策略不知道“当前实际处于自动机的哪个状态”语义会复杂化。确定性 Büchi 自动机并不能接受所有 ω-regular 语言所以实践中常用确定性奇偶自动机或确定性 Rabin 自动机。工具方面Spot 的ltl2tgba、Owl、ltl2dstar、Rabinizer 都可以完成这类转换。4.2 构建乘积 MDP设 MDP 的状态为 s自动机的状态为 q。乘积状态是 (s,q)。每执行一个动作 aMDP 转移到 s同时根据 s 满足的原子命题集合更新自动机状态 q δ(q, L(s))。乘积 MDP 的转移概率继承原始 MDP 的转移概率。对于一个 LTL 公式 φ原问题“MDP 中满足 φ 的最优概率”就等价于“乘积 MDP 中满足自动机接受条件的最优概率”。对于 parity 条件接受语义变成轨迹上无限次出现的最大颜色编号是偶数。这个转换是精确的没有信息损失。4.3 端部组件与接受条件问题到这一步还没有完全解决。对于 Büchi、parity 这类长期目标值迭代如果直接套用折扣奖励的算法往往不收敛或收敛到错误值。原因是状态空间中存在端部组件end componentEC即一组状态在某个策略下可以无限保持在其中且概率质量不再离开。为了正确计算长期目标的概率必须先找出极大端部组件MEC并把接受条件映射到端部组件上一个端部组件是“接受”的当且仅当它包含接受条件对应的状态。在鲁棒 MDP 中端部组件的处理还要额外小心。因为转移概率是不确定的某个端部组件是否“几乎必然可达”取决于最坏情况下的概率下界而不是名义概率。也就是说原本在普通 MDP 里一个简单的图论可达性判断在鲁棒 MDP 里需要结合区间概率重新分析。5. 工具链与环境准备5.1 推荐工具工具定位适用场景PRISM经典概率模型检验器普通 MDP、LTL/概率 CTL 性质验证算法正确性Storm高性能概率模型检验器大规模 MDP、部分版本支持鲁棒模型检验C 与 Python 绑定SpotLTL 与 ω-自动机库LTL 转自动机、自动机化简、DPA 构造Owl / ltl2dstar / Rabinizer自动机转换工具生成确定性 Rabin/parity 自动机自研 Python算法原型验证理解算法、小规模实验、定制鲁棒集合5.2 运行环境建议使用 Linux 或 WSL2。Python 环境建议 3.8 以上安装以下依赖即可跑通本文示例pip install numpy scipy spotPRISM 需要从官网下载对应平台的压缩包不同操作系统安装方式不同这里不做版本写死以官方安装文档为准。Storm 推荐用官方 Docker 镜像或者按 GitHub 仓库的构建说明编译Python 绑定也可以从源码构建。版本细节不展开是因为这些工具迭代较快写死版本对读者反而没有意义。6. 完整示例与代码实现6.1 示例问题带区间不确定性的三状态鲁棒 MDP我们构造一个最小但完整的例子。状态 0 是起点状态 1 是目标吸收态状态 2 是失败吸收态。在状态 0 有两个动作动作 a到达目标概率在 [0.7, 0.8]失败概率在 [0.1, 0.2]留在原地的概率在 [0, 0.2]。动作 b到达目标概率在 [0.5, 0.6]留在原地的概率在 [0.2, 0.4]失败概率在 [0, 0.3]。目标是最小化最坏情况下到达目标状态的概率。这个例子的好处是可以用手算验证设 v0 为状态 0 的鲁棒值v11v20。动作 a 的最坏概率会尽可能把质量分给失败态和起点得到 v 0.7 0.1×v0动作 b 得到 v 0.5 0.2×v0。比较后动作 a 更优解方程 v0 0.7 0.1×v0得到 v0 0.7778。6.2 代码一鲁棒值迭代实现下面是一份完整可运行的 Python 实现重点在inner_min_expectation函数它用贪心算法求解区间集合下的内层最小期望。# file: robust_mdp_example.py import numpy as np def inner_min_expectation(lo, hi, v): 求解 min_{p: lo p hi, sum(p)1} p v 区间 单纯形约束下贪心分配即可得到最优解。 思路概率先按下界放置剩余质量优先分配给 v 最小的状态。 n len(v) p lo.copy() remaining 1.0 - p.sum() for i in sorted(range(n), keylambda idx: v[idx]): if remaining 1e-12: break add min(hi[i] - lo[i], remaining) p[i] add remaining - add return float(p v), p def robust_value_iteration(states, actions, lo, hi, eps1e-8, max_iter10000): # 状态 1 是目标吸收态值固定为 1状态 2 是失败吸收态值固定为 0 v np.zeros(len(states)) v[1] 1.0 transient [s for s in states if actions[s]] for it in range(max_iter): v_new v.copy() for s in transient: best -np.inf for a in actions[s]: e, _ inner_min_expectation(lo[s][a], hi[s][a], v) best max(best, e) v_new[s] best diff np.max(np.abs(v_new - v)) v v_new if diff eps: return v, it 1 return v, max_iter states [0, 1, 2] actions {0: [0, 1], 1: [], 2: