概率模型检查

冗余服务轨迹 ​

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

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

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

共用随机数是构造方法，边缘等式才是证书 ​

设一个组件尚未失效时下一步失效概率为 $p$，另一个为 $q\ge p$。可共同抽 $U\sim \mathrm{Unif}[0,1]$：第一个在 $U\le p$ 时失效，第二个在 $U\le q$ 时失效。较可靠组件失效时，另一组件也失效，因而能逐条路径比较“某时刻前已失效”的事件。

但“使用同一随机数”本身没有验证力；要明确映射和概率。若强行让两条链始终取相同的新状态，却只按 $p$ 抛硬币，第二条链的失效概率会被改成 $p$。这种伪证书看似保持相等，实际不满足第二边缘。

两条吸收失效链的完整证书 ​

状态 $0$ 表示正常，$1$ 表示已失效且不再修复。令 $0\le p\le q\le 1$，

在全部四个配对状态上给出联合核；表外没有其他转移：

例如 $00$ 行中，第一边缘转到 $0$ 的概率为 $(1-q)+(q-p)=1-p$，转到 $1$ 为 $p$；第二边缘转到 $0$ 为 $1-q$，转到 $1$ 为 $(q-p)+p=q$。$01$ 行第一边缘为 $(1-p,p)$、第二边缘恒为 $1$；$10$ 行相反地让第一边缘恒为 $1$、第二边缘为 $(1-q,q)$；$11$ 行两个边缘都吸收。非负性和每行归一化也逐项成立。

关系 $R=\{00,01,11\}$ 即 $x\le y$。初态在 $R$，上述三行都不进入 $10$，故关系保持。取 $A=$“第一条链截至第 $n$ 步（含）已失效”、$B=$“第二条链截至第 $n$ 步（含）已失效”，逐点次序直接给出事件蕴含，所以前者概率不超过后者。

令 $p=1/4,q=1/2$，完整可达分布为：

第二步的 $01$ 质量为 $(1/2)(1/4)+(1/4)(3/4)=5/16$，$11$ 质量为 $(1/2)(1/4)+(1/4)(1/4)+1/4=7/16$。独立计算单链也得到 $1-(3/4{)}^2=7/16$ 与 $1-(1/2{)}^2=3/4$，核验两个边缘。

终态不等与路径曾经不等 ​

两状态空间相同时，任意终态事件 $A\subseteq S$ 满足

因为在相等时两个指标一致。对所有事件取上确界就是总变差上界。[5, §2.2] 本例只有 $01$ 不相等，由 $\text{Pr}(X_n=0)=(1-p{)}^n$ 和 $\text{Pr}(Y_n=0)=(1-q{)}^n$ 得

在 $n=2$，失效事件的差本身就是 $5/16$，故终态上界取到等号。

若 $A$ 依赖整个有限前缀，直接的耦合论证必须改成

在本例中，首次分歧必须在仍停于 $00$ 时走 $00\to 01$，这些首次时刻互斥，故右边为

$n=2$ 时是 $1/4+(1/2)(1/4)=3/8$。其中路径 $00\to 01\to 11$ 的概率为 $1/16$：它曾经不等，终态却相等，正好解释 $3/8-5/16$。这是本联合构造给出的路径上界，不宣称它是路径分布间最小可能距离。

两链从 $00$ 出发已经相等，之后仍可分离，因为 $P\ne Q$。因此不能把“首次相遇时间”代入通常相遇后锁合的耦合界。另若使用独立转移耦合，边缘依然正确，但在 $00$ 会以 $p(1-q)$ 的概率进入 $10$，在本例中它等于 $1/8>0$，不能用它证明次序不变量。

MDP 与调度器 ​

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

对有限 MDP，先约定每个状态的动作集非空。目标 $G$ 的最大到达概率在 $s\in G$ 上为一，在 $s\notin G$ 上满足 Bellman 方程

最大到达概率是带上述目标边界条件的最小非负解；不能仅因某个向量满足方程就认定它是所求概率。

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

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

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

有限核证书的检查边界 ​

给定有理数表，检查者逐行验证非负性、归一化、两项边缘等式，再验证联合初始分布的非负性、归一化、两项初始边缘等式及 ${\lambda }_0(R)=1$，并对每个 $(x,y)\in R$ 检查 $K((x,y),R^c)=0$。事件蕴含仍须由事件定义证明；有限时域可以枚举路径或采用积状态记录事件。接受这些义务后，前述有限和证明给出可靠的概率比较，无须采样猜测。

若允许每步至多 ${\epsilon }_t$ 的概率离开关系，必须另外累积坏事件质量；不能继续使用严格不变量的概率一结论。若模型包含调度非确定性，联合核还要与所声称的两侧调度器量词一致。本页证书固定两个随机矩阵，不直接证明任意 MDP 的最优概率比较。

奖励与长期性质 ​

给状态或转移附 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 校正。若校正权重错误，估计可有极低表面方差却系统偏置；模拟加速仍需统计证明。

从有限概率模型转向可不终止的程序时，次概率程序语义公理库次概率程序语义Subprobabilistic program semantics将概率程序解释为输入到终止输出的次概率核，用缺失质量记录不终止，并逐步计算顺序组合。用缺失输出质量保存非终止概率。做状态约简时，概率互模拟公理库概率互模拟Probabilistic bisimulation按等价类总转移概率定义有限 Markov 链的强互模拟，算出可合并状态并展示概率差异如何被观察。则要求到每个等价类的总质量一致；只保留相同出边支撑会漏掉概率差异，不能保证约简后的定量性质正确。