Fast Computation of Conditional Probabilities in MDPs and Markov Chain Families

技术摘要：马尔可夫决策过程与马尔可夫链族中条件概率的快速计算

问题陈述
本文解决了在马尔可夫决策过程（MDPs）中计算最优条件可达概率的挑战。虽然马尔可夫链（MCs）上的条件可达性可通过贝叶斯定理有效处理，但将其扩展到 MDPs 则十分困难，因为分子（同时到达目标 $G$ 和证据 $E$）的最优策略与分母（到达证据 $E$）的最优策略通常不同。目前最先进的标准方法——“重启方法”（Baier 等人 [7]）——通过将无法到达 $E$ 的状态的转移重新连接到初始状态，将该问题简化为标准的可达性查询。然而，这种变换即使在原本无环的 MDPs 中也会引入循环，从而产生对标准求解器（如值迭代）而言极具挑战性的实例，并经常导致数值不稳定或性能低下。

方法论
作者提出了一种基于多目标模型检测和总奖励查询的替代方法，避免了引入循环。核心方法包含三个主要步骤：

1. 基于总奖励的阈值判定：
   为了判定 $\Pr^{\max}_M(\diamond G \mid \diamond E) \le \lambda$，作者利用源自贝叶斯定律的关键观察：
   $$\max_{\sigma} \Pr_\sigma(\diamond G \mid \diamond E) \le \lambda \iff \max_{\sigma \in \Sigma_{M,E}} \left( \Pr_\sigma(\diamond G \cap \diamond E) - \lambda \cdot \Pr_\sigma(\diamond E) \right) \le 0$$
   这将条件问题转化为最大化两个可达概率的线性组合。该表达式被重新表述为一个期望总奖励问题。定义了一个奖励函数 $R_\lambda$，使得到达 $E$ 中的状态产生的奖励基于随后到达 $G$ 的概率，而到达 $G$ 中的状态产生的奖励基于随后到达 $E$ 的概率。

2. 预处理与初始分量消除：
   为了确保总奖励查询定义良好且可解，作者对 MDP 进行了预处理：

   • $G \cup E$ 中的状态被设为吸收态。
   • 定义了一组终止状态 $T$（$E$ 中的状态以及 $G$ 中能到达 $E$ 的状态）。
   • 关键在于，算法识别出一个“初始分量”（$CI$），由那些在某些策略下无法以正概率到达$T$ 的状态组成。通过构建一个新的 MDP（$\tilde{M}$）并显式建模从 $CI$ 退出的转移，这些状态被消除。这确保了新 MDP 中的所有策略都能以正概率到达 $T$，从而允许应用标准的总奖励算法（如值迭代或线性规划），而无需担心未定义的条件概率问题。

3. 通过二分法优化：
   为了计算最优值（问题 2），阈值判定过程被嵌入到二分法算法中。作者引入了几项优化：

   • 精确计算： 使用 Stern-Brocot 树遍历来寻找具有最小分母的有理数。
   • 策略追踪： 如果同一个策略在二分区间的下界和上界均诱导最优值，则无需进一步迭代即可立即计算出精确的最优值。
   • 高级边界： 利用预先计算的 $E$ 的可达概率来收紧二分搜索的边界。

4. 与抽象 - 细化（彩色 MDP）的集成：
   该方法被扩展用于分析表示为彩色 MDP（策略必须保持颜色一致）的马尔可夫链族。作者调整了抽象 - 细化框架 [3] 以处理条件属性。他们指出，基于访问计数的标准细化启发式方法并不直接适用；相反，他们采用了一种关注与初始状态距离的向后细化策略。

主要贡献

• 新算法： 一种数值稳定、无环的 MDP 条件可达性到总奖励查询的归约方法。
• 复杂度： 对于无环 MDP，阈值问题可在线性时间（$O(\|M\|)$）内判定，这比引入循环的重启方法有了显著改进。
• 策略提取： 一种提取条件属性最优策略的技术，这些策略不一定无记忆，从而能够集成到抽象 - 细化循环中。
• 可扩展性： 通过彩色 MDP 和抽象 - 细化同时分析数百万个马尔可夫链的能力。

结果
作者在 Storm 模型检测器中实现了该方法，并在来自贝叶斯网络、概率程序和运行时监控的 318 个基准测试中与重启方法进行了评估。

• 性能： 新方法（"treat"）相比重启方法实现了多个数量级的加速，特别是在无环基准测试和具有大型初始分量的基准测试上。
• 准确性： 重启方法在标准基准测试上经常无法收敛或产生显著的数值误差。新方法在浮点运算和精确算术中均提供了准确的结果。
• 彩色 MDP： 在彩色 MDP 的背景下，新方法显著优于重启方法，解决了此前超时的基准测试。
• 运行时监控： 在运行时监控实验中，新方法将平均评估时间从秒级降低到亚秒级，使其适用于监控器的学习和部署。

意义
本文声称在计算 MDP 上的条件概率方面取得了“显著进展”。通过摒弃重启方法的循环归约，作者实现了对条件可达性的高效、稳定且精确的分析。这使得将条件推理应用于建模为 MDP 的复杂系统成为可能，包括具有不确定参数的系统（贝叶斯网络）和具有大量配置族的系统（彩色 MDP）。这项工作弥合了理论多目标模型检测与实际高性能验证工具之间的差距。