概率模型检测

读书笔记
123 留言

对《Principles of Model Checking》一书概率模型检测部分的翻译。

未完成 先鸽了

模型检测技术一般着眼于绝对保证的正确性——“系统的失败是不可能的”——事实上，这种僵化的概念很难保证，或者说是不可能保证的。事实上，系统受制于一种随机性的多种现象，比如消息丢失或者混淆之类的，所以正确性——“99%概率上个系统不会失败”——正在变得没那么绝对。这一章节讨论了概率系统，也就是表现出概率性的系统，的自动化验证。概率层面对下面几种情况是非常至关重要的：

  • 随机算法。 经典案例是分布式算法比如领导人选举或者共识算法（使用抛硬币实验打破过程之间的“对称性”，从而最终以概率1达成共识。）
  • 对不可靠和不可预测系统行为的建模。比如消息丢失、处理器故障等现象可以用不确定性来进行建模。这通常适用于早期系统设计阶段，在该阶段中，系统被认为是高度抽象的，并且未明确指定有关可能性的信息（有时是故意的）。 但是，在以后的设计阶段中，内部系统的特征将变得更加占主导地位，概率是量化并改进此信息的有用工具。
  • 基于模型的性能评估。由于性能评估旨在预测系统性能和可靠性，概率信息-消息传输延迟的分布是什么或处理器的故障率是多少？ —需要存在以评估定量属性，例如等待时间，队列长度，故障间隔时间等

为了建模随机现象，转移系统被赋予概率。这通过不同的几种方式实现。在离散时间的马尔科夫链（MCs）中，所有的选择是概率性的。马尔科夫链是最常用的用来评估信息处理系统的性能和可靠性的互操作模型。概括的讲，马尔科夫链就是对每个状态后继者的概率分布的转移系统。换句话说，下个状态会概率的进行选择，而不是不确定的进行选择。马尔科夫链不适用于随即分布式系统的建模，因为他们无法以适当的方式对并发系统的交错行为进行建模。为了这个目的，马尔科夫决策进程（Markov decision processes，MDPs）被使用。在MDPs中，不确定性和概率性选择共存。简而言之，MDPs是一个任何状态下，概率分布之间都存在一个不确定性选择的转移系统。一旦不确定性的选择了概率分布，就如同MCs中一样，将以概率方式选择了下一个状态。因此，任何MC都是在任何状态下唯一确定概率分布的MDP。随机分布算法通常都由MDP进行合适的建模，因为概率影响算法的只是一小部分，而不确定性用于进程之间进行交互的并发行为的建模。

概率系统的验证可以集中在定量性质或定性性质（或两者）上。 定量属性通常会限制某些事件的概率或期望。 定量属性的实例是，例如，要求在接下来的t个时间单位内传递消息的概率至少为0.98，或者在并发系统中寻找领导者的不成功尝试的预期次数最多为7。 另一方面，定性属性通常断言某个（好）事件几乎肯定会发生，即概率为1，或者两次断言，某个（坏）事件几乎不会发生，即概率为零。 马尔可夫模型的典型定性属性是可达性，持久性（最终是否总是会发生事件？）和重复可达性（是否可以重复达到某些状态？）

本章节目的是介绍离散时间的马尔科夫链和马尔科夫决策进程的定性和定量性质的主要验证原理。从分析可达性、持久性和重复可达性到CTL的概率性变体模型检测算法，称为概率计算树逻辑，简称为PCTL。此逻辑适用于以一种非常优雅的方式，表示一大类属性。例如属性“最终一个领导者将会以至少4/5的概率当选”在PCTL中将会被表述为：

另一种表述为：

断言在所有6个中间配置c为非空的情况下，接下来6个步骤里通道被完全占用的概率被限制在0.015

除了PCTL中的分支时间属性之外，本章还介绍了线性时间属性。在PCTL中，概率是通过 $\mathbb{P}$ 运算实现的，在线性时间设置中，概率概念仅仅出现在语义级别上。也就是说，在概率线性时间设置中，LTL公式用于指定所需的或者不好的行为，目的是建立给定的LTL公式成立的概率。因此，状态之间的满足关系不再是布尔值——公式在某个状态下是否满足——而是将一个概率值分配给了状态。本章涉及线性时间属性的验证，例如正则安全属性和$\omega$安全属性。

与本专论的其余部分一致，我们采用了基于状态的概率模型视图。这意味着将马尔科夫链和马尔可夫决策过程视为有向图的变体。在该变体中，边（转移过程）使用随机信息进行赋值。这与许多教科书中将MC定义为随机变量序列相反。当将MCs和MDPs视作一个反应系统和时态逻辑结构的操作模型时，基于状态的方法（具有针对状态的原子命题）似乎更自然。由于马尔可夫模型的组合方法不在本专论的讨论范围之内，因此本章不涉及任何操作，因此将其省略。

马尔科夫链

马尔科夫链表现为转移系统，唯一不同指出在于后继状态之间的不确定性选择被概率性选择所代替。也就是说，状态s的后继状态会根据概率分布进行选择。该概率分布仅仅取决于当前状态s，而不取决于比如从某些初始状态引导到该状态s的路径片段。因此，系统演变不取决于历史（即到目前为止已经执行的路径片段），而仅仅取决于当前状态s。这被称为无记忆属性。

定义1. （离散时间的）马尔科夫链（MC）

一个（离散时间的）马尔科夫链是一个五元组$\mathcal{M} = (S,\mathbf{P},\iota_{init},AP,L)$，其中

  • S是一个可数的、不为空的状态集合

  • $\mathbf{P}$：$S \times S \rightarrow [0,1] $是转移概率函数，对于所有状态s，有

  • $\iota{init}$:$S \rightarrow [0,1]$是初始分布，$$ \sum\limits{s\in S} \iota_{init}(s)=1 $$

  • AP是一个原子命题的集合，$L:S\rightarrow2^{AP}$是一个标签函数

当$S$和$AP$是有限的时候，$\mathcal{M}$被称为有限的。对有限的$\mathcal{M}$,$\mathcal{M}$的大小（表示为$size(\mathcal{M})$)指的是状态的数量加上$(s,s’)$对的数量，其中$(s,s’)\in S \times S$并且$\mathbf{P}(s,s’)>0$。

转移概率函数$\mathbf{P}$指定了每个状态s的概率$\mathbf{P}(s,s’)$，该概率描述的是从再单独的一次转移中，状态$s$移动一步到$s’$的概率。==施加在$\mathbf{P}$上的约束确保$\mathbf{P}$是分布的。对于马尔可夫链的数学处理，非零的转移概率是否合理是无关就要的。==然而，处于算法目的，我们假定$\mathbf{P}(s,s’)$的值对于所有的状态$s,s’\in S$都是合理的。

$\iota{init}$的值指定系统从状态s开始进行的概率。$\iota{init}(s)>0$的状态s被视作初始状态。类似的，$\mathbf{P}(s,s’)>0$的状态s‘被视为s的可能后继。对于状态$s$和$T\subseteq S$，令$\mathbf{P}(s,T)$表示从状态s转移一步到达某个状态$t\in T$的概率。也就是说，

在==续集（sequel）==中，我们通常用矩阵$(\mathbf{P}(s,t)){s,t\in S}$来标识转移概率函数$\mathbf{P}:S\times S\rightarrow [0,1]$。矩阵中状态$s$的行$\mathbf{P}(s,·)$包含从$s$转移到其后继的概率，而状态$s$的列$\mathbf{P}(·,s)$指定从任何其他状态进入状态$s$的概率。类似的，初始分布$\iota{init}$通常被视作一个向量$(\iota{init}(s)){s\in S}$。

原子命题和标记函数$L$的使用和转移系统相同，本章的其余部分，我们通常将状态名视作原子命题，比如$AP = S$并且$L(s)={s}$。

当且仅当$\mathbf{P}(s,s’)>0$时，马尔科夫链才会产生一个底层有向图，其中状态充当顶点，并且从s到s’有一条边。在底层有向图中，马尔科夫链中的路径是最大（比如无限）路径。他们被定义为对所有$i\geq0$下$ \mathbf{P}(s_i,s_i+1)>0$的无限状态序列$\pi = s_0 s_1 s_2 ···\in S^{\omega} $。对于$\mathcal{M}$中的路径$\pi$ ，$inf(\pi)$表示在$\pi$中被无限经常次访问的状态集。对于有限马尔科夫链，$inf(\pi)$对所有的路径$\pi$非空。

马尔科夫链由他们的底层有向图表示，其中边上被赋予了[0,1]之间的转移概率。如果状态s有一个唯一后继s’，比如$\mathbf{P}(s,s’)=1$，那么可以省略转移概率。

示例2. 一个简单的通信协议

考虑一个使用通道的简单的通讯协议。参见图中的马尔可夫链，从消息可能会丢失的角度来看，这是非常容易出错的。在此，对于$s \neq start$，$\iota{init}(start)=1$并且$\iota{init}(s)=0$，即$start$是独一无二的初始状态。在$start$状态，一条消息被生成并沿着通道被发送给独一无二的后继状态$try$。这个消息会有$\frac{1}{10} $的概率丢失，那么消息会被重新发送，知道它最终被发送到。一但消息被正确地发送，系统会返回它的初始状态。

image.pngimage.png

使用针对$start,try,lost,delivered$等状态的枚举，转移概率函数$\mathbf{P}$被看作一个$4\times 4$矩阵，初始分布被看作一个列向量。

路径的一个示例为

沿着这条路径，每条消息在送达之前要被重发两次。它是遵循$inf(\pi)=S$。对于$T={lost,delivered}$,我们有$\mathbf{P}(try,T)=1$。

示例3. 用公平硬币来模拟骰子

考虑由Knuth和Yao最初提出的使用公平硬币来模拟6面骰子的行为，可以得到如图所示的马尔科夫链：

image.pngimage.png

计算从初始状态$s0$开始，即对于所有状态$s\neq s_0$，我们有$\iota{init}(s0)=1$并且$\iota{init}(s)=0$。底层的1，2，3，4，5和6状态表示了可能的骰子结果。每个内部节点表示扔了一个公平的硬币。如果结果为正面，左侧分支确定下一个状态，如果结果为反面，右侧分支确定为下一个状态。

如果处于状态$s0$时的抛硬币实验产生的结果为正面，则系统迁移至状态$s{1,2,3}$，再次投掷硬币以相等的概率导向状态$s{2,3}$(该状态骰子会以相等的概率产生2或者3) 或者状态$s’{1,2,3}$。从后面这种状态出发，投掷硬币会以$\frac{1}{2}$的概率产生1，或者以$\frac{1}{2}$的概率返回状态$s_{1,2,3}$。在初始状态下产生结果为反面的行为导致的结果是对称的。我们将会在后面对此进行确定，事实上，这个马尔科夫链可以充分地对一个骰子进行建模，即结果具有同等可能性。

示例4. 掷骰子赌博游戏

游戏掷骰子时基于对两个骰子掷骰结果的投注。第一次投掷出来的结果决定是否需要再投一次。当结果投出来为7或11，游戏结束，玩家获胜，结果投出来为2，3或者12是”残次“，玩家输了。投出来的 结果为其他情况时，再投一次，但是第一次投出来的结果已经留存了（也就是点数）。如果下一轮投掷出7点或者上次投掷的点数，游戏结束，为7点时，玩家输掉，为上次投出来的点数时，玩家获胜。其他任何情况下，继续投骰子，直到最终获得7点或者那个结果位置。如图描述了掷骰子游戏行为的马尔科夫链。状态$start$是唯一的初始状态。我们有$\mathbf{P}(start,won)=\frac{2}{9}$,因为有8种成功的掷骰组合:$(1,6),(2,5),(3,4),(5,6)$以及相应对称的组合。其他转移概率以类似的方式确定。状态4，5，6，8，9和10处的自环回路对骰子的重新投掷进行建模。对于$T={4,5,6}$，我们有$\mathbf{P}(s_0 ,T)=\frac{1}{3}$。

image.pngimage.png

示例5. Zeroconf协议

IPv4的Zeroconf协议是为了家庭局域网应用（微波炉、笔记本电脑、VCR、DVD放映机等）设计的，每种设备都配有网络接口以实现相互通信。这样的自组织网络必须是热插拔并且可以自我配置的。覆盖所有这些应用，意味着将新设备（接口）连接到网络时，必须为其自动配置一个唯一的IP地址。Zeroconf协议以下述几种方式解决这个任务。主机需要从65024个可选地址中随机选择一个IP地址，比如说$U$进行配置，然后广播一条消息（称之为探测）“谁在使用地址$U$?”如果探测被一个已经在使用地址$U$的主机收到，它就会通过一条消息进行答复，表示$U$已经在使用了。收到此消息后，需要配置的主机重新启动：它再次随机挑选一个新的地址，广播一个探测信号······

由于消息丢失或者主机繁忙，一个探测或者回复消息可能不能到达某些（或者所有）主机。为了增强协议的可靠性，一个主机需要发送$n$个探测信号，每个后面都要跟着一个$r$个时间单位的监听周期。因此，主机仅仅可以在n个探测都被发送，并且在$n·r$个时间单位内没有到回复之后，开始使用选择的IP地址。注意，在协议运行之后，主机仍然有可能会使用一个另外的主机正在使用的IP地址，如果说所有的探测都被丢失了。这种被称为地址冲突的情况是非常不希望的，因为他可能迫使主机终止活跃的TCP/IP链接。

image.pngimage.png

单个主机的协议行为由包含$n+5$个状态的马尔科夫链进行建模（$n=4$的情况如上图所示），其中$n$时需要的探测的最大数量（如上所述）。初始状态是$s0$（标记为$start$）。在状态$s{n+4}$中（标记为$ok$），主机最终使用一个未被使用的IP地址并结束；在状态$s{n+2}$中（标记为$error$），主机使用一个正在使用的IP地址并结束，也就是地址冲突。状态$s_i(0<i\leqslant n)$在发射第$i$个探测后到达。在状态$s_0$主机随机选择一个IP地址。概率$q = m/65024$，其中m是链接入网络的主机的数量，这些地址是正在使用的。主机有$1-q$的概率选择一个未被使用的地址并且在状态$s{n+3}$结束。然后它在使用这个地址之前，要发射$n-1$个探测并且等待$n·r$个时间单元。（发送的这些探测以及等待时间从MC中抽象）。如果哦选择的IP地址已经是正在使用的了，就会进入状态$s_1$。现在两个情形是可能的。在$r$个时间单元内，有$p$概率什么回复都没有收到（因为探测信号或者应答信号已经丢失），并且下一个探测信号已经发送，那么就进入状态$s_2$。但是，如果一个应答及时被收到了，那么主机就会返回初始状态并且重新启动协议。这些状态$s_i(2\leqslant i <n)$的行为是类似的。但是如果在状态$s_n$中，没有应答在发送了第$n$个探测信号后的$r$个单元时间内被收到，那个一个地址冲突就发生了。

我们采用转移系统中的直接后继和直接前驱的概念，令$Paths(\mathcal{M})$表示在马尔科夫链$\mathcal{M}$中的路径，$Pahts{fin}(\mathcal{M})$表示有限路径片段$s_0s_1···s_n$的集合，其中$n\geqslant0$并且$\mathbf{P}(s_i,s{i+1})>0$对于所有的$0\leqslant i0}$。同理,$Pre(s)={s’ \in S | \mathbf{P}(s’,s)>0}$。$Post^(s)$表示所有从状态$s$通过一个有限路径片段到达的状态结合，$Pre^(s)={s’\in S | s \in Post^*(s’)}$。对于$B\subseteq S$,令

注释6. 吸收状态

如果$Post^(s) = {s}$，那么马尔科夫链$\mathcal{M}$的状态s被称为吸收*。如果$\mathbf{P}$是一个随机矩阵，每一行的总和等于1，那么当且仅当$\mathbf{P}(s,s)=1$并且对于所有的$t\neq s$有$\mathbf{P}(s,t)=0$，$s$是一个吸收状态。

备注7. 离散时间马尔科夫链
示例8. 扔公平的硬币
定义9. Cylinder 集
定义10. 马尔科夫链的$\sigma$-代数
示例11. Cylinder 集
注释12. 事件的LTL风格表示

可达性概率

示例13. 按无穷级数计算可达性概率
示例14. 简单通信协议
理论15. 最小不动点表征
备注16. 膨胀法
备注17. 选择$S{=0}$和$S{=1}$
备注18. 几种不动点
理论19. 独特的解决方案
备注20. 矩阵$I-A$的非奇异性
示例21. 掷骰子游戏中的可达性受到限制
备注22. 暂态（Transient）概率
示例23. 暂态概率的可达性

定性属性

备注24. 重复可达性和持久性的可测量性
理论25. 概率选择作为强公平性
注释26. 马尔可夫链的图形符号
理论27. 马尔可夫链的极限行为
示例28. Zeroconf协议（修订版）
理论29. 几乎可以确定的可达性
推论30. 全局几乎可以确定的可达性
推论31. 定性约束可达性
示例32. 定性约束可达性
推论33. 定性重复可达性
推论34. 定量重复可达性
备注35. 无限马尔科夫链的定性性质

概率计算树逻辑（Probabilistic Computation Tree Logic ）

定义36. PCTL语法
示例37. 在PCTL中指定属性
定义38. PCTL的满足关系
引理39. PCTL事件的可衡量性

PCTL模型检测

理论40. MC的PCTL模型检测的时间复杂度
示例41. 反例

PCTL的定性片段

定义42. PCTL的定性片段
定义43. 等价的PCTL和CTL公式
引理44.
引理45.
引理46. 几乎可以肯定的重复可达性是PCTL定义的
理论47. 重复可达概率是PCTL定义的
理论48. 持久性概率是PCTL定义的

线性时间性质

定义49. LT属性的概率
定义50. 产品马尔科夫链
理论51. 安全性的定量分析
理论52. DBS可定义属性的定量分析
定义53. 确定性拉宾自动机（DRA）
示例54. $\square \lozenge a$的DRA
理论55. DRA和$\omega- $正则语言
理论56. 基于DRA的马尔科夫链分析
备注57. $\omega-$正则性质的可测量性
理论58.

PCTL* 和 概率互模拟

PCTL*

定义59. PCTL*语法

概率互模拟

定义60. 马尔可夫链的互模拟
示例61. 马尔可夫链的互模拟
定义62. 互模拟商
示例63. 掷骰子游戏

有代价的马尔科夫链

成本受限的可达性

长期属性

马尔可夫决策过程

可达性概率

PCTL模型检测

限制属性

线性时间性质和PCTL*

公平性

总结