计算机软件是信息基础设施的灵魂,它已经渗透到国民经济、国防建设和个人生活的各个方面^[1].软件系统正变得日趋庞大和复杂,很多实际的软件系统被赋予随机行为特征^[2],其原因可分为3类:

(1) 系统本身包含随机性,如概率算法或随机化算法(randomized algorithm)的使用;

(2) 系统运行环境的复杂,造成系统构件间调用过程的失败或传递消息的丢失等随机故障的发生;

(3) 对系统进行性能评价和分析,需要人为地增加随机变量来刻画其相应的性能指标.

用模型检验(model checking)^{[3, 4, 5]}的方法对具有随机行为的复杂系统进行定量验证,即称为随机模型检验(stochastic model checking)或概率模型检验(probabilistic model checking)^{[6, 7]}.

随机模型检验是经典模型检验理论的延伸和推广,可对随机系统进行基于模型的自动的形式验证.

近年来,随机模型检验引起了形式验证等领域的广泛关注,取得了较大的进展,其代表性成果有:英国牛津大学Kwiatkowska课题组的PRISM、德国亚琛工业大学(RWTH Aachen University)Katoen课题组的MRMC和德国萨尔兰大学(Saarland University)Hermanns课题组的PARAM等.目前,随机模型检验已开始应用到概率程序的正确性验证^[8]、系统性能分析^[9]、通信协议可靠性分析^[10]、服务流程的服务质量优化^[11],甚至系统生物学^[12]等领域.

由于随机模型检验算法结合了经典模型检验算法和线性方程组求解或线性规划算法等,并且其运算处理的是关于状态的概率向量而非经典模型检验中的位(bit)向量,所以状态爆炸问题(state explosion problem)在随机模型检验中更为严重^{[6, 9]}.因此对于规模较大的随机系统,如何缓解状态爆炸问题,将随机模型检验应用于此类软件系统的定量验证和分析,是随机模型检验研究面临的一个重要挑战.在Turing Lecture中,图灵奖得主Clarke把如何缓解随机模型检验中的状态爆炸问题列为模型检验未来研究领域的一个重要方向^[6].

抽象技术^[13]作为一种有效的缓解状态爆炸问题方法,在经典模型检验中取得了较好的效果.其实,抽象方法在软件工程的其他很多领域也扮演着重要的角色^[14],如对于无限状态系统进行模型检验验证、建模开放系统运行环境的非确定性因素、构件组合式软件的规约和软件模型检验等.本文将以缓解随机模型检验中状态爆炸问题的模型抽象技术为研究对象,对其进行分类、总结和论述.

本文第1节给出本文中所用到的随机模型检验的基本概念.第2节给出面向随机模型检验的模型抽象问题描述.第3节对随机模型检验的模型抽象技术分类和归纳.第4节总结对比目前的模型抽象技术,并指出应对模型抽象挑战的几种未来的研究方向.

1 随机模型检验的基本概念

随机模型检验将经典模型检验的系统模型扩展到随机系统模型,将描述功能性质的时序逻辑扩展到可同时描述功能和性能的定量时序逻辑.目前,可验证的随机系统模型有DTMC(discrete-time Markov chain,离散时间马尔可夫链)、CTMC(continuous-time Markov chain,连续时间马尔可夫链)、MDP(Markov decision process,马尔可夫决策过程)、PA(probabilistic automata,概率自动机)、NPPN(Nondeterministic Probabilistic Petri net,非确定概率Petri网)^[15]、PTA(probabilistic timed automata,概率时间自动机)^{[16, 17]}、CTMDP(continuous-time MDP,连续时间马尔可夫决策过程)^{[18, 19]}和IMC(interactive Markov chain,交互式马尔可夫链)^[20]等,其分类见表 1.

在随机系统模型中,DTMC,CTMC和MDP是基本的随机系统模型,它们与其他随机系统模型的关系如图 1所示,其定义如下:

定义1(DTMC). DTMC可定义为M=(S,P,s₀,AP,L),其中,

· S是可数的非空状态集合,表示被建模系统的所有可能配置状态;

· P:S×S→[0, 1]是迁移概率函数,对于$\forall s \in S$, $\sum\nolimits_{s' \in S} {P(s,s') = 1} $表示被建模系统状态间迁移的概率值;

· s₀是初始状态;

· AP是原子命题的集合;

· L:S→ 2^AP是标号函数,可用于表示用户的需求,即系统应该满足的性质.

定义2(CTMC). CTMC可定义为M=(S,R,s₀,AP,L),其中,

· S,s₀,AP,L表示的含义与DTMC相似;

· R:S×S→$\Re $_≥0是退出速率(exit rate)函数,$\Re $_≥0是非负实数.

定义3(MDP). MDP可定义为M=(S,Act,s₀,AP,L),其中,

· S,s₀,AP,L与DTMC定义的含义相似;

· Act表示动作的集合,P:S×Act×S→[0, 1]是迁移概率函数,对于$\forall s \in S$,动作a∈Act,$\sum\nolimits_{s' \in S} {P(s,a,s') \in \{ 0,1\} } .$

目前,可验证的定量时序逻辑有PCTL(probabilistic computation tree logic,概率计算树逻辑)、LTL+ probability bounds(linear temporal logic with probability bounds,带有概率界的线性时序逻辑)、CSL(continuous stochastic logic,连续随机逻辑)、PCTL*、PTCTL(probabilistic timed computation tree logic,概率时间计算树逻辑)^[21]和某些定量时序逻辑的动作扩展(如aCSL^[22],asCSL^[23-25],aPCTL^[15],asPCTL^[26])等.其分类见表 2.

在定量时序逻辑中,PCTL,LTL,PCTL*和CSL是基本的定量时序逻辑,其他定量时序逻辑均可看作是它们的扩展或综合,其定义如下:

定义4(PCTL). 关于原子命题集合AP的PCTL状态公式$\Phi $可定义为

$\Phi :: = true\left| a \right|\Phi \wedge \Phi \left| {\neg \Phi } \right|{P_{ \sim p}}(\Psi )$

其中,a∈AP,$\Psi $是路径公式,~∈{≤,<,≥,>},p∈[0, 1]是概率界限值;

PCTL路径公式$\Psi $可定义为

$\Psi :: = X\Phi \left| {\Phi \cup \Phi } \right|\Phi { \cup ^{ \le n}}\Phi $

其中,X(next)和∪(until)与CTL路径运算符语义相同,∪^≤n(bounded until)是∪的变体,要求n次迁移或小于n次迁移内满足∪语义,n是非负整数,$\Phi $是状态公式.

定义5(LTL). LTL公式$\Psi $可定义为

其中,a∈AP,AP是原子命题集合.LTL公式最终是一个路径公式,其他的路径公式可以由定义推出.

$\Psi :: = true\left| a \right|\Psi \wedge \Psi \left| {\neg \Psi } \right|X\Psi \left| {\Psi \cup \Psi } \right.$

定义6(PCTL*). 关于原子命题集合AP的PCTL*状态公式$\Phi $可定义为

$\Phi :: = true\left| a \right|\Phi \wedge \Phi \left| \neg \right.\Phi \left| {{P_{ \sim p}}\left( \Psi \right)} \right.$

其中,a∈AP,$\Psi $是路径公式,~∈{≤,<,≥,>},p∈[0, 1]是概率界限值;

PCTL*路径公式$\Psi $可定义为

$\Psi :: = \Phi \left| {\Psi \wedge \Psi } \right|\neg \Psi \left| {X\Psi } \right|\Psi \cup \Psi \left| {\Psi { \cup ^{ \le N}}\Psi } \right.$

其中,$\Phi $是状态公式,n是非负整数.

定义7(CSL). 关于原子命题集合AP的CSL状态公式$\Phi $可定义为

$\Phi :: = true\left| a \right|\Phi \wedge \Phi \left| {\neg \Phi } \right|{P_{ \sim p}}(\Psi )\left| {{S_{ \sim P}}(\Phi )} \right.$

其中,a∈AP,$\Psi $是路径公式,~∈{≤,<,≥,>},p∈[0, 1]是概率界限值;

路径公式$\Psi $可定义为

$\Psi :: = X\Phi |\Phi { \cup ^I}\Phi ,$

其中,$\Phi $是状态公式,I是一个实数区间.

2 面向随机检验的模型抽象问题描述

随机模型检验是通过穷尽遍历随机系统模型判定其是否满足给定的定量性质规约,包含3个元素,可表示为M$\Phi $,其中,M是随机系统模型,如DTMC,MDP,CTMC等;$\Phi $是用定量时序逻辑表示的定量性质规约,如PCTL, PCTL*,LTL+概率等;是基于算法的满足关系判断.而基于抽象的随机模型检验(关于统一的基于抽象的随机模型检验理论可参见文献[14])是指在对任一随机模型检验元素抽象的基础上进行的随机模型检验,可表示为M^α=^α$\Phi $^α,其中,M^α是抽象的随机系统模型,^α是基于算法抽象的满足关系,$\Phi $^α是抽象的定量性质规约.其实,抽象模型往往会导致算法抽象和定量性质规约抽象;抽象算法也会导致定量性质规约的抽象,文献[27, 28, 29, 30, 31]均可看作是对算法进行的抽象的研究;抽象定量性质规约也可能会导致模型抽象和算法抽象,但关于定量性质规约本身的抽象研究较少^[14].

面向随机检验的模型抽象,是通过验证比原具体模型小的抽象模型来实现验证原具体模型,即,通过M^α$\Phi $相关的信息得到M$\Phi $相关的信息,其过程如图 2所示.

抽象技术的目标是使抽象模型拥有足够小的状态空间却包含丰富的具体系统模型信息,但是模型抽象的过程往往会引起模型相关信息丢失,理想的模型抽象技术要满足以下条件:

(1) 抽象模型M^α要明显小于原具体模型M;

(2) M^α$\Phi $→M$\Phi $,M^α$\Phi $→M$\Phi $.

因此,面向随机检验的模型抽象主要面临以下问题,我们称其为MA4SMC(model abstraction for stochastic model checking)问题:

① 如何构造和表示抽象模型?

② 如何随机模型检验验证抽象模型?

③ 能够验证哪些定量性质?

④ 如何表示抽象模型验证中的反例?

其中,如何回答MA4SMC问题①是实现基于抽象的随机模型检验方法的关键,它将影响后续问题②~问题④的解决方法和结果.

3 模型抽象研究方向及进展

本节我们按照MA4SMC问题①的解决方法对模型抽象技术进行分类总结,分析其满足理想抽象技术条件的程度,并论述其目前主要的研究进展.

3.1 基于模拟关系的抽象 3.1.1 强概率互模拟

强概率互模拟^[32]也称为概率互模拟,是对LTS(labelled transition system,标号迁移系统)上的强互模拟^{[33, 34]}的定量扩展,即,强概率互模拟状态到其他每个在强概率互模拟下的等价类状态,要拥有相同的迁移概率.

定义8(强概率互模拟). 令M=(S,P,s₀,AP,L)是一个DTMC,在M上的强概率互模拟是关于S的等价关系R,且对于任意(s₁,s₂)∈R,满足以下条件:

(1) L(s₁)=L(s₂);

(2) 对于每个等价类C∈S/R,P(s₁,C)=P(s₂,C),其中,$P({s_i},C) = \sum\nolimits_{c \in C} {P({s_i},c)} .$

如果(s₁,s₂)∈R,R是M上的强概率互模拟,则状态s₁和s₂称为强概率互模拟等价,可标记为s₁~_M s₂.

在CTMC上的强概率互模拟定义^[35],需要将条件(2)变成:R(s₁,C)=R(s₂,C),其中,$R({s_i},C) = \sum\nolimits_{c \in C} {R({s_i},c)} {\rm{.}}$在MDP上的强概率互模拟定义^[36],需要对每个非确定性选择的动作Act,存在一个动作选择使其满足条件(2).

强概率互模拟可以减少具体模型的状态空间,达到抽象目的,其用强概率互模拟商来表示抽象模型.

定义9(强概率互模拟商). 令M=(S,P,s₀,AP,L)是一个DTMC,M的强概率互模拟商可定义为

M/~=(S',P’,AP,s₀,L'),

其中,S’=S/~={[s]_~|s∈S},[s]_~表示状态s的强概率互模拟状态;P'([s]_~,C)=P’(s,C);L'([s]_~)=L(s).

在文献[37]的基础上,文献[38]最早给出了自动构造DTMC.M的强概率互模拟商M/~的算法,即划分-精化算法,其算法步骤如下:

(1) 根据标号函数,对具体模型状态进行初始划分为{S₁,S₂,…,S_n},集合S_i中的状态满足相同的标号函数;

(2) 找出需要状态分离的集合S_i,即,若s,s'∈S_i,对于某集合S_k,P(s,S_k)≠P(s',S_k);

(3) 把集合S_i划分为子集合,使每个子集合中的状态到达S_k的概率一致;

(4) 重复步骤(2)、步骤(3),直到没有可划分的状态集合为止.

通过划分-精化算法可得到最粗糙的(coarsest)强概率互模拟商,但其依赖于初始划分,即,在初始划分时没有在一个状态集合的某些状态将不会得到其等价关系.

如表 3所示,基于强概率互模拟等价的抽象,用M/~表示抽象模型,用划分-精化算法来构造抽象模型.其优点是可保持PCTL*/CSL性质^[39],即,对于此类性质满足理想抽象技术条件(2),模型检验M/~得到的结果与模型检验M得到的结果是一致的;其缺点是抽象模型状态空间过大,且构造抽象模型的时间有可能超过模型检验具体模型的时间.为此,文献[40]采用组合的方法,将具体模型的强概率互模拟分解为子构件的强概率互模拟,并将其用于POTS(plain-old telephone system)的定量分析;文献[41]首次用基于MTBDD(multi-terminal binary decision diagrams)的符号算法实现构造DTMC的商模型,其在时间上和处理大规模状态空间上均表现出了较好的优势;文献[42]利用互模拟求解器(satisfiability modulo theories,简称SMT)从PRISM建模语言直接构造最粗糙的互模拟商,避免了在求商模型之前要构造整个模型的状态空间;文献[43]以概率自动机为随机系统模型,在定义了强1步互模拟及强分支互模拟的基础上给出了一种新的强概率互模拟概念,与目前的强概率互模拟相比,其可在保持PCTL*性质前提下得到最小的强概率互模拟商模型.

3.1.2 弱概率互模拟

与强概率互模拟相比,弱概率互模拟^{[44, 45]}是一种较为粗糙的模拟关系,可以得到较小的抽象模型.

定义10(弱概率互模拟). 令M=(S,P,s₀,AP,L)是一个DTMC,在M上的弱概率互模拟是关于S的等价关系R,且对于任意(s₁,s₂)∈R,满足以下条件:

(1) L(s₁)=L(s₂);

(2) 对于每个等价类C∈S/R,C≠[s₁]_R,[s₁]_R表示状态s₁的弱概率互模拟状态,s₁可到达[s₁]_R以外的状态当且仅当s₂可到达[s₂]_R以外的状态,并且P(s₁,C)/(1-P(s₁,[s₁]_R))=P(s₂,C)/(1-P(s₂,[s₂]_R)),如果P(s_i,[s_i]_R)<1, i=1,2.

如果(s₁,s₂)∈R,R是M上的弱概率互模拟,则状态s₁和s₂称为弱概率互模拟等价,可标记为s₁≈_M s₂.

与强概率互模拟类似,MDP上的弱概率互模拟^[43]及弱概率互模拟商的定义均可做相应的修改而得到.

弱概率互模拟可保持不包含X(next)路径运算符的PCTL*性质,即,此类性质满足理想抽象技术条件(2),其虽然可以得到较小的抽象模型,但构造抽象模型需要计算可达概率,其算法复杂度较高.对于DTMC,文献[44]给出了构造抽象模型的3次方复杂度算法;对于MDP,文献[46]给出了构造抽象模型的指数级算法;直到2012年,文献[47]给出了构造抽象模型的多项式算法.

3.1.3 强概率模拟

强概率模拟^{[32, 48]}可以看作是强模拟^{[49, 50]}的定量扩展,即,强概率模拟状态的分布(distribution)需要匹配(match)其模拟状态的分布.分布的概念可以用权函数(weight function)^[48]来刻画.

定义11(权函数). 令Dist(S)表示关于状态集合S的分布集合,μ,μ'∈Dist(S),R$ \subseteq $S×S,F∈Dist(S)是一个(μ,μ')

和R的权函数,需要满足以下条件:

(1) F(s,s')→(s,s')∈R;

(2) $\mu (s) = \sum\nolimits_{s' \in S} {F(s,s')} ;$

(3) $\mu (s') = \sum\nolimits_{s \in S} {F(s,s')} .$

如果存在(μ,μ')和R的权函数,可标记为μ$ \subseteq $_Rμ'.

定义12(强概率模拟). 令M=(S,P,s₀,AP,L)是一个DTMC,R$ \subseteq $S×S是强概率模拟,则对于任意(s₁,s₂)∈R,满足以下条件:

(1) L(s₁)=L(s₂);

(2) P(s₁,*)$ \subseteq $_RP(s₂,*),$P({s_i},*) = \sum\nolimits_{s \in S} {P({s_i},s)} .$

如果(s₁,s₂)∈R,R是M上的强概率模拟,则状态s₁和s₂称为强概率模拟等价,可标记为s₁$\begin{array}{*{20}{c}} \prec \\ \sim \end{array}$_M s₂.

在CTMC上的强概率模拟定义^[51]需要满足的条件是:

(1) 其嵌入式DTMC满足强概率模拟;

(2) s₂要具有比s₁更快的退出速率.

在MDP上的强概率模拟定义^[36]需要对每个非确定性选择的动作Act,存在一个动作选择使其满足条件(2).

强概率模拟也是用其商M/$\begin{array}{*{20}{c}} \prec \\ \sim \end{array}$^{[51, 52]}表示抽象模型,可保持PCTL*中的定量安全真值性质,即,满足理想抽象技术条件(2)的M^α$\Phi $→M$\Phi $;但与强概率互模拟相比,其得到的抽象模型的状态空间较小.其构造抽象模型的算法也是基于划分-精化思想.对于DTMC和CTMC,文献[51]已经证明,强概率模拟等价与强概率互模拟是一致的,因此构造抽象模型的时间复杂度类似.对于MDP,其强概率模拟商严格粗糙于强概率互模拟商,其构造算法涉及到参数最大流算法(parametric maximum flow algorithm)^[53],文献[52, 54]对此做了一些改进工作.

3.1.4 弱概率模拟

弱概率模拟^{[51, 55]}是模拟关系中最为粗糙的模拟关系,其定义和构造商模型的过程与上述模拟关系类似.弱概率模拟同样用商表示抽象模型,得到的抽象模型也较小,可保持不包含X(next)路径运算符的PCTL*的定量安

全真值性质,即,此类性质满足理想抽象技术条件(2)的M^α$\Phi $→M$\Phi $,但其时间复杂度也较高^{[52, 54]}.目前,关于基于弱概率模拟的抽象研究文献较少.

3.2 基于偏序化简的抽象

偏序化简^{[56, 57, 58, 59]}是基于并发操作的执行顺序一般不会改变系统性质,固定一种交替执行的顺序可以减少系统模型的状态和迁移数目.因为依赖和独立关系体现了迁移发生之间的偏序关系,所以相应的方法称为偏序化简.直到近七八年,足够集(ample set)^{[57, 60]}的偏序化简方法才开始用于随机模型检验中的模型抽象.

足够集偏序化简方法的大体思想是:对于MDP M的任一状态s,令其足够集为ample(s)$ \subseteq $Act(s),然后用ample(s)来替代Act(s)构造偏序化简的MDP $\hat M$ $\hat M$即为偏序化简的抽象模型,可定义为$\hat M = (\hat S,Act,\hat P,{s_0},AP,\hat L){\rm{,}}$

其中,

· $\hat S \subseteq S{\rm{,}}$包括初始状态s₀和状态{t|P(s,a,t)>0,$s \in \hat S$,a∈ample(s)};

· $\hat L:\hat S \to {2^{AP}};$

· $\hat P(s,a,t) = \left\{ {\begin{array}{*{20}{l}} {P(s,a,t),}{{\rm{if }}a \in ample(s)}\\ {0,}{{\rm{if }}a \notin ample(s)} \end{array}} \right..$

足够集定义所能满足的条件,决定了化简后的抽象模型可保持定量性质的范围.文献[61]率先将足够集的偏序化简方法引入到随机模型检验,其针对MDP特性,对经典的足够集条件^{[57, 60]}进行了扩充,要求足够集必须满足以下5个条件:

(1) 非空条件,即,对于任一s∈S,$\Phi $≠ample(s)$ \subseteq $Act(s);

(2) 哑(stutter)条件,即,如果$s \in \hat S$并且ample(s)≠Act(s),那么所有的动作a∈ample(s)均为哑动作;

(3) 依赖条件,即,对于每条路径,并且γ依赖于ample(s),存在一个i∈{1,…,n},使得a_i∈ample(s);

(4) 终端分量条件,即:在模型$\hat M$的每个终端分量(T,A)中存在一个状态s∈T,满足ample(s)=Act(s);

(5) 分支条件,此为新增条件,即,如果在存在M中的一条路径,其中,$s \in \hat S$,a₁,…a_n,γ$ \notin $ample(s)并且γ是概率的,那么|ample(s)|=1.

其实,文献[61]中的条件(4)是对经典足够集条件(4)的弱化.在经典足够集条件中,条件(4)为循环条件,即,对于$\hat M$中的每条路径,存在一个状态s_i使得ample(s_i)=Act(s_i).文献[61]定义的足够集条件使偏序化简后的抽象模型与原具体模型的关系是概率哑等价(probabilistic stutter equivalence),可保持不带X算子的概率界的LTL性质.文献[62]加强了文献[61]新增的足够集条件(5),将其变为:对于任一状态$s \in \hat S{\rm{,}}$ample(s)=Act(s)或者ample(s)是单一元素的集合.文献[62]定义的足够集条件使偏序化简后的抽象模型与原具体模型的关系是完全向前概率模拟(complete forward simulation),可保持最大概率可达的定量性质和不带X算子的概率界的LTL性质,该方法已经在工具LiQuor^[63]中使用基于动态深度优先搜索算法on-the-fly产生化简模型实现.文献[64]进一步加强了文献[61]新增的足够集条件(5),将其变为:对于任一状态$s \in \hat S{\rm{,}}$满足ample(s)=Act(s)或者ample(s)={a}且a是非概率动作.其实,该条件是文献[56]为实现两个非概率系统模型间的可视互模拟定义的.文献[64]定义的足够集条件使偏序化简后的抽象模型与原具体模型的关系是弱概率互模拟关系,可保持不带有X算子的PCTL*性质.

虽然文献[61, 62, 64]加强了足够集条件并将其用于随机模型抽象,但实验结果显示,状态和迁移的化简过程和顺序与应用于非随机模型抽象一样^{[65, 66]},其过程的局限性在于需要用线性规划求解显式表示的化简模型.针对上述问题,文献[65]以静态偏序化简^[67-69]为基础,首次将偏序化简与静态分析技术结合应用于MDP模型化简,给出了一个基于静态偏序化简的随机模型抽象框架:将化简标准插入到系统的控制流图,并用通过分析和修改概率控制流图算法来实现对应的标准,其可保持哑不变量的定量线性和分支时间性质.

与用足够集用于随机模型偏序化简不同,文献[70]首次将固执集(stubborn set)^[71]方法用于随机模型化简,给出了一种基于弱固执集的MDP模型的偏序化简方法,并用on-the-fly化简和最优的Tarjan算法^[72]在PRISM^[73]中实现了原型工具,其可以保持无条件公平性定量性质和公平调度下的最大概率可达性质.

3.3 基于对称化简的抽象

对称化简^{[74, 75, 76, 77]}是利用系统模型本身具有的状态对称重复特点对其进行化简,其本质是计算系统模型在不同局部状态对称构件的个数.对称在很多随机系统模型中均有所体现,如随机分布式算法、通信协议和生物系统等.

定义13(状态对称). 令M是一个DTMC,Δ:S→S是变换函数,若Δ满足P(Δ(s),Δ(s'))=P(s,s'),则s和s'是对称状态.

在CTMC上的对称状态的定义,只需将P变成退出速率函数R;在MDP上的对称状态定义,需要对非确定性求解后,要求其满足定义中的条件.

对称化简通过合并对称的状态达到抽象目的,基于对称化简的抽象用商表示抽象模型.

定义14(对称商). 对于一组关于状态S的变换函数G和相应的orbit关系θ,化简后的DTMC商模型可定义$(\bar S,\bar P)$,其中,$\bar S$是包含每个orbit等价类一个代表状态,$\bar P(\bar s,\bar s') = \sum\nolimits_{\{ s' \in S|rep(s') = \bar s'\} } {P(\bar s,s')} {\rm{,}}$函数rep:$S \to \bar S$用来为每一个状态s选择一个对应的代表状态$rep(s) \in \bar S,\bar s,\bar s' \in \bar S.$

关于CTMC和MDP的对称商,可根据相应的状态对称定义得到.

基于对称化简的抽象用其商表示抽象模型,商模型与原具体模型是强概率互模拟关系^[28],因此其可保持PCTL*或CSL性质,但构造对称商要比构造概率互模拟商所花费代价小.文献[78]扩展了文献[79, 80, 81]的方法,给出一种了面向建模语言层面的随机模型的对称化简方法,把对称化简和MTBDD的符号表示结合在一起,定义了PRISM建模语言关于DTMC和MDP语义的对称子集SP(symmetric PRISM),并开发了工具GRIP^[82],自动地将SP模型转化为化简的模型.文献[83]采用动态对称化简^{[84, 85]}的方法给出了一种面向模型层面的随机模型对称化简方法,将其用于DTMC,CTMC和MDP模型抽象,提出了基于MTBDD的一种高效构造对称商模型的算法,并将其在PRSIM工具中实现.文献[86]认为:由于建模语言的限制约束的存在,以文献[78]为代表的面向语言层面的随机模型的对称化简方法很难用于复杂模型的化简.因此,文献[86]扩展了文献[78]的工作,提出了一种表达能力更强的SPSL(symmetric probabilistic specification language)及其对应的求解抽象模型的转换算法,并在工具GRIP中实现,转换后的模型可以直接用PRISM工具验证.文献[87]把对称化简的抽象方法引入到显式状态的随机模型检验,提出一种较为完整的基于对称化简的随机模型抽象方法:定义了功能较为强大的PSS语言(probabilistic symmetric system language),通过抽取图,给出了自动发现PSS对称结构的方法,借助爬山算法和局部求解算法给出了有效的计算PSS对称等价类方法,并用改造的图遍历算法,可以直接从PSS构造对称商模型.

3.4 基于概率反例引导精化的抽象

上述抽象技术得到的抽象模型过于细化,即,抽象模型的状态空间并无明显减少,且对无限状态随机系统模型的抽象效果不理想.为此,基于概率反例引导精化的抽象(概率反例引导的抽象精化)把缓解经典模型检验中状态爆炸问题的CEGAR(counterexample-guided abstraction-refinement)^[88]技术应用于随机系统模型的抽象,其关键是如何定义反例和表示抽象模型,抽象模型本质上属于存在抽象(existential abstraction)^[89].如图 3所示,基于概率反例引导精化的抽象是一个自动化过程,其大体思想是:先构造一个较为粗糙的随机系统模型的抽象模型,用随机模型加以检验,用检验结果的无效反例增量精化初始的抽象模型,直到验证的性质在抽象模型上正确或者是产出了经过确认的有效反例.

文献[89]可看作其雏形,文献[90]以PRISM语言规约的MDP为随机系统模型,用MDP作为抽象模型,使用类似路径结构的DTMC作为反例,通过基于插值的谓词推理来分析反例,给出了第一种概率反例引导精化的抽象方法,并实现了相应的工具PASS^[91],但其只能保持最大可达定量性质.文献[92]针对文献[90]保持性质范围的限制,并指出其原因是反例定义包含的信息不充分.为此,文献[92]使用图状结构MDP作为反例,给出了多项式时间的反例生成算法,用MDP作为抽象模型,提出了一种可验证PCTL定量安全和活性性质的概率反例引导精化的抽象方法.

3.5 基于误差引导精化的抽象

如图 4所示,基于误差引导精化的抽象(误差引导的抽象精化)也是一种自动的抽象精化过程,过程本质上与基于概率反例引导精化的抽象有相似之处,其主要区别在于:该方法以抽象获得的误差(上界与下界的差别)作为抽象模型的精确度,如果误差过大,则需要精化抽象模型.

文献[93]可以看作是基于误差引导精化的抽象方法的雏形,其用MDP模型作具体MDP模型的抽象模型,只能保持最大概率可达类定量性质,其精化终止的条件是从抽象模型得到的可达概率满足给定的阈值,并实现了相应工具RAPTURE.但由于该方法只能产生可达概率最小值的下界或最大值的上界这种方法,或许其更适合于DTMC模型的抽象.

针对MDP作为MDP抽象模型的不足——只能产生可达概率最小值的下界或最大值的上界,文献[94]首次提出用随机博弈^[95]作为MDP的抽象模型,以区别原具体模型MDP的不确定性和因抽象形成的新的不确定性,其可以同时得到可达概率最小值或最大值的上下界.但是文献[94]方法的自动化程度不高,需要手动地划分模型状态空间.为此,文献[96]在文献[90, 92, 93, 94]的基础上,给出了一种完整的自动的基于误差引导精化的抽象方法,其可看作是在文献[90, 92]的抽象精化框架下,用文献[94]中的抽象模型表示方法、用文献[91]的精化方法精化抽象模型.文献[96]的方法已被用来扩展工具PASS^[97],可以使其快速得到较小的抽象模型.但是文献[96]的方法也有局限性,即,只能验证定量可达性质,目前甚至还不能用于PCTL定量安全性质验证.

3.6 基于不确定结果引导精化的抽象

在文献[90, 92, 94, 96]的抽象精化方法中,文献[92]是可保持性质范围最大的方法,但其也只能保持PCTL定量安全/活性的真值性质,即,抽象模型满足此性质,则原具体模型也满足此性质;若抽象模型不满足此性质,原具体模型也有可能满足此性质.基于不确定结果引导精化的抽象(3值抽象精化)技术可以弥补上述不足,其用3值抽象方法^{[98, 99]}扩展抽象-精化框架,大体思想如图 5所示.

文献[100]最先给出随机模型的3值抽象精化方法,以DTMC作为随机系统模型,用概率区间^[101]表示迁移概率:给出一种抽象马尔可夫链模型(abstract Markov chain,简称AMC)并用其表示抽象模型,区间下界可用于表示下界逼近(under approximation),区间上界可用于表示上界逼近(over approximation)信息,原具体模型与抽象模型间依然是概率模拟关系;给出了PCTL的3值语义及其随机模型检验AMC算法,其可保持PCTL性质,即,此类性质满足理想抽象技术条件(2),但验证结果有可能是不确定结果.

文献[102]将文献[100]的方法应用于CTMC抽象.文献[103, 104]对文献[100, 102]的方法进行了改造和扩展,针对其抽象过程中的不精确性,研究了规范化DTMC和统一化CTMC的3值抽象方法,为随机模型的3值抽象提供了严格的理念基础.

4 总结与展望

本文以随机模型检验中的模型抽象技术为研究对象,对其进行了问题描述,归纳了其主要的研究方向和进展.在模型抽象技术中,每种技术均有其优点和缺点,很难同时满足理想的模型抽象技术的两个条件.它们之间的对比和关系如下:

(1) 基于模拟关系的抽象是最基本的抽象技术,其他抽象技术往往可以归结为某种概率模拟关系.

(2) 概率互模拟、对称化简、偏序化简属于准确抽象,其构造的是一个等价抽象模型,可保持的性质范围较大,但抽象模型过于细化造成其状态空间没有明显比原具体模型小;其余抽象技术属于近似抽象,其构造的抽象模型较为粗糙,但可保持的性质范围较小.

(3) 对于准确抽象,抽象模型往往与原具体模型属于同一类模型,其随机模型检验过程和求解反例方法可以使用一般的随机模型检验理论验证和反例求解.对于近似抽象,抽象模型是MDP的可直接使用一般的随机模型检验理论验证和反例求解;抽象模型是随机博弈模型的可用线性规划或值迭代等方法求解,但尚未涉及反倒求解;抽象模型是AMC的要用3值随机模型检验方法验证,但也没有反例相关研究.

(4) 在准确抽象技术中,基于对称化简和偏序化简的抽象技术只能对具备相应特点的随机系统模型进行抽象.

(5) 在近似抽象技术中,以MDP和AMC作为抽象模型,其拥有相同规模的抽象模型状态空间.但AMC作为抽象模型会使其迁移变少,且其抽象程度更高,即概率界限值精确程度低.

(6) 在近似抽象技术中,除3值抽象外,其余抽象技术均可看作是2值语义抽象范畴,其本质上属于存在抽象,是对具体模型的上界逼近,即,抽象模型比具体模型拥有更多的行为;而3值抽象则可以同时对具体模型进行上界逼近和下界逼近,但需要定义相关的3值抽象模型及其3值时序逻辑语义和与之相应的随机模型检验算法.

虽然目前面向随机模型检验的模型抽象技术已取得了一定的进展,但其要么是可保持性质范围太小,要么构造的抽象模型过于细化,即,还没能给出解决MA4SMC问题的满意答案.我们认为,可以从以下几个方面来应对上述挑战:

(1) 抽象技术的完备性理论

面向随机模型检验的抽象技术的最基础理论是,该抽象技术是否具有完备性和有效性.完备性是指:若具体模型M满足性质$\Phi $,则存在一个小的有限状态模型M^α作为模型M的抽象,且M^α满足性质$\Phi $;有效性是指:若抽象模型M^α满足性质$\Phi $,则具体模型M满足性质$\Phi $.目前的抽象技术研究仅涉及到其有效性,除文献[105, 106]之外,还几乎没有关于完备抽象技术的研究工作.

(2) 抽象技术本身的优化

1) 寻找更好的概率模拟关系定义及其有效的构造商模型的算法,使得抽象模型状态空间少且包含更丰富的信息.以下文献对该问题做了一些尝试工作:文献[107]用抽象解释^{[108, 109]}刻画概率互模拟和概率模拟,为算法求解概率互模拟和概率模拟提供了一个通用框架,并基于此给出了一种新的高效的概率模拟算法;文献[43]给出了一种新的关于PLTS(probabilistic labeled transition system)的概率互模拟和概率模拟定义,使其可以准确地刻画PCTL*逻辑等价.

2) 加强/消弱足够集满足的条件,寻求偏序化简可满足性质范围与抽象模型状态空间大小间的平衡.

3) 在抽象-精化技术中,研究更好的方法来实现精化抽象模型,如局部精化^[110]或者启发式引导精化的抽象技术.

4) 组合抽象技术,将组合验证方法,如假设-保证推理与抽象精化技术相结合,形成组合式抽象精化方法,如文献[111, 112]的工作属于这一方向的探索.

(3) 抽象技术的融合或集成

抽象技术各有其优缺点,可以考虑将两种或两种以上抽象技术集成使用,以扬长避短,得到更好的抽象 结果:

1) 概率互模拟与抽象精化方法的集成,如文献[106]用增量计算may/must商来自动实现抽象精化 方法.

2) 偏序与对称方法的融合,偏序化简是去掉随机系统模型的迁移冗余,而对称化简是去掉随机系统模型的冗余状态,这为将两种方法融合提供了理论上的可能性.

(4) 新的随机模型抽象技术

研究针对随机系统模型的新的抽象技术,是应对挑战的重要方法.如,文献[66, 113]定义了一种新的关于概率自动机的confluence概念,并证明基于confluence化简的抽象可保持分支互模拟,并可以on-the-fly使用;学习算法^[114]在经典模型检验的抽象中取得了较好的效果,并且文献[115]的研究已说明,学习算法用在构造随机模型的可行性.我们认为,基于学习算法的抽象在随机模型的抽象中应该会有所作为.

(5) 抽象技术应用于其他缓解状态爆炸问题的方法

1) 假设保证推理式组合随机模型检验.假设保证推理式组合随机模型检验^{[112, 116]}的关键是产生假设,理论上,抽象技术可用于产生假设^[112].

2) 限界随机模型检验.限界随机模型检验^{[29, 30]}是通过搜索有限步长随机模型的反例,得到验证结果的方法.目前的抽象-精化方法仅应用于一般的随机模型检验,若将其用于限界随机模型检验,应该会使限界随机模型检验更快,并且也可以用限界随机模型检验产生精化需要的相关信息.

(6) 抽象技术应用范围的扩展

目前,面向随机模型检验的抽象技术还只是用于基本的随机系统模型,如DTMC,CTMC和MDP,虽开始应用于概率时间自动机验证^[117],但对于一些复杂的或high-level的随机系统模型,还有待进一步地研究如何将抽象技术应用于此类随机模型的验证,如连续时间马尔可夫决策过程^{[18, 19]}、交互式马尔可夫链^[20]、随机混成系统模型^[118]、非确定概率Petri网^[15]和随机多人博弈模型^[119]等.

致谢　本文的工作得到江苏省软件新技术与产业化协同创新中心的资助,在此表示感谢.