概率模型检查

概率转移模型 ​

离散时间 Markov 链写作

$$\mathcal{D}=(S,P,I,L),$$

其中 $P(s,s^{\prime })\in [0,1]$ 且对每个 $s$ 有 $\sum _{s^{\prime }}P(s,s^{\prime })=1$。它复用Markov 链公理库Markov 链Markov chain未来条件分布在给定当前状态后与更早历史无关的随机过程。的路径测度，并以状态标记 $L$ 解释逻辑命题。

路径公式 $\psi$ 诱导可测路径事件，概率算子可写成

$${\mathsf{P}}_{\ge p}[\psi ].$$

状态 $s$ 满足该公式，当从 $s$ 出发的路径中满足 $\psi$ 的概率公理库概率分布Probability distribution · Law定义在可测空间上的概率测度；随机变量的律是由推前得到的一类分布。至少为 $p$。

这扩展普通模型检查公理库模型检查问题Model checking problem · Model checking给定系统模型与形式规格，判定所有指定初始行为是否满足公式，并交付证明结果或诊断见证。的布尔答案：工具可以计算精确或有误差界的概率，再与阈值比较。

到达概率方程 ​

目标集合为 $G$。最终到达 $G$ 的概率 $x_s$ 满足

$$x_s=1(s\in G),$$$$x_s=\sum _{s^{\prime }}P(s,s^{\prime })x_{s^{\prime }}(s\notin G).$$

对不可能到达 $G$ 的状态置零，在剩余状态上解线性方程或用 value iteration。若链含不进入 $G$ 的 bottom SCC，简单把所有非目标状态初始化为一并迭代可能收敛缓慢，预处理图结构很重要。

线性方程的解是语义对象；浮点求解的舍入和停止误差还需给上下界，尤其当结果接近阈值 $p$ 时不能用未经证明的近似直接判真。

冗余服务轨迹 ​

两个独立组件每轮各以概率 $0.01$ 失效，系统在两个都失效时进入 down。若模型只做一轮，失败概率是 ${10}^{-4}$；多轮允许修复或持久故障时，状态必须记录每个组件当前健康性，不能把单轮概率重复相乘而忽略状态。

从 (up,up) 到四种健康组合的概率由乘积给出，下一轮再按当前组合转移。目标 reachability down 的概率通过上述方程累计所有不同时间的首次失败路径。

若两组件共享电源，独立性假设错误，乘积模型会严重低估风险。概率模型检查忠实计算模型分布，不验证分布参数和独立假设来自现实。

MDP 与调度器 ​

Markov decision process 同时含非确定动作与概率后继。固定 scheduler 后才得到路径概率测度，因此性质通常询问

$$\underset{\sigma }{inf}{\text{Pr}}_s^{\sigma }(\psi ),\underset{\sigma }{sup}{\text{Pr}}_s^{\sigma }(\psi ).$$

最大到达概率满足 Bellman 方程

$$x_s=\underset{a\in Act(s)}{max}\sum _{s^{\prime }}P(s,a,s^{\prime })x_{s^{\prime }}.$$

把非确定选择平均成均匀概率擅自加入策略，会得到另一个模型。最坏、最好和某个控制策略下的概率必须分别报告。

对有限 MDP reachability，存在 deterministic memoryless scheduler 达到最优值，但这项结论依赖目标和模型类型。带多目标、部分可观察或历史约束的策略可能需要随机化或记忆，不能把 reachability 特例推广到所有概率规格。

若 scheduler 能观察现实控制器看不到的隐藏状态，计算出的最优概率不可实现。部分可观察模型必须限制策略信息，问题复杂度也会改变。

奖励与长期性质 ​

给状态或转移附 reward，可检查到目标前期望成本、有限时域累计奖励或长期平均。期望有限需要到达性和无正成本逃逸循环等条件；存在永不到目标的正概率时，expected time 可能为无穷。

稳态概率只对适当遍历类有唯一极限。多 bottom SCC 的链会让长期分布依赖初态和吸收概率，不能无条件输出一个全局稳态向量。

连续时间 Markov 链用 rate matrix $R(s,s^{\prime })$；离开状态的等待时间呈指数分布，总 exit rate 决定驻留时间。把 rate 直接归一化成离散概率只保留下一跳，丢失时间界性质。CSL 的 bounded until 需结合 uniformization 或瞬态分析。

reward 若在状态驻留期间按时间累计，CTMC 的期望奖励还要乘停留时间；把它当每跳固定奖励会得到另一个量。

PCTL、CSL 等逻辑分别服务离散/连续时间模型；时间界、next 和 until 的语义随模型改变，不能把公式名字相同当成完全可互换。

误差界与阈值判断 ​

value iteration 得到近似向量 $x^{(n)}$ 时，迭代差小不自动给出到真解的误差界，尤其在近吸收慢混合链中。可靠工具可维护单调下、上界 $l_n\le x\le u_n$，只有当两界都落在阈值同侧才返回布尔结论。

若 $p$ 落在 $[l_n,u_n]$ 内，应继续计算或返回 unknown；用打印小数四舍五入后比较会把数值误差伪装成概率证明。

参数概率模型中的转移含未知参数，结果可能是有理函数或分段区域。代入一个标称参数得到的答案不能代表整个允许区间。

统计估计的不同保证 ​

statistical model checking 通过采样估计满足概率，给置信误差而非穷举式精确结果。它适合状态巨大模拟器，却可能漏极稀有反例；样本独立、停止规则和显著性都要写入保证。不能把 Monte Carlo “未观察到失败”称为传统概率模型检查已证明零概率。

稀有事件 importance sampling 会改变采样分布并用 likelihood ratio 校正。若校正权重错误，估计可有极低表面方差却系统偏置；模拟加速仍需统计证明。

参考资料

• Christel Baier and Joost-Pieter Katoen, Principles of Model Checking, MIT Press, 2008, Chs. 10–11。
• Hans Hansson and Bengt Jonsson, “A Logic for Reasoning about Time and Reliability,” Formal Aspects of Computing 6, 1994, pp. 512–535。
• Marta Kwiatkowska, Gethin Norman, and David Parker, “PRISM 4.0: Verification of Probabilistic Real-Time Systems,” CAV, 2011, pp. 585–591。