基于决策图的复杂系统模型对称约减方法

纪明宇，王海涛，陈志远，李艳梅

（1.东北林业大学 信息与计算机工程学院，黑龙江 哈尔滨150040；2.哈尔滨工程大学 计算机科学与技术学院，黑龙江 哈尔滨150001）

0 引 言

作为一种重要的自动验证技术，模型检测［1］因其可以自动执行，并能在系统不满足性质时提供反例路径等优点而在软、硬件系统的性能验证方面应用日益广泛。然而随着待验证系统模型的不断增大，状态爆炸的问题在很大程度上制约着模型检测技术的进一步应用，现有的抑制状态爆炸问题的技术主要有：符号模型检测［2］、约减技术［3］等。其中符号模型检测技术利用有序二元决策图 （ordered binary decision diagrams，OBDD）对模型的状态空间进行压缩表示，然而OBDD只能表示布尔函数，对于支持复杂参数特征性质定量分析验证的概率模型［4，5］状态空间爆炸问题并不适用。

与符号模型检测不同，约减技术利用系统行为中的等价关系减少本质上相同的重复路径，在传统模型检测及概率模型中得到了很好的应用［6，7］，文献 ［8］将对称约减技术应用于连续时间马尔可夫链 （continuous time Markov chain，CTMC）和马尔可夫判定过程 （Markov decision process，MDP）模型，并给出了实例分析，但未对支持迁移资源描述的随机模型约减方法进行说明。

本文将结合符号模型检测与对称约减技术，使其应用于支持迁移资源消耗的概率模型中，使用改进的多终端二元决策图表示状态迁移矩阵，基于对称约减理论给出针对迁移矩阵的约减算法，并给出实例说明。

1 基本概率模型

定义1 DTMC

DTMC为五元组Μ ＝ （S，P，L，AP，v），其中S表示状态集合，P：S×S→［0，1］为状态转移概率矩阵，对于状态集的状态s，有 ∑s＇∈Sp（s，s＇）＝1，L：S→2AP为状态标记函数，AP表示原子命题的有限集，v∈Distr（S）为初始分布集合。

下面基于DTMC给出支持迁移回报的离散时间Markov 判 定 过 程 （Discrete Time Markov Rewards Decision Process，DTMRDP）的定义。

定义2 DTMRDP

DTMRDP为七元组M ＝ （S，A，P，L，AP，N，v），它是在原有的DTMC的基础上增加了迁移动作集合A和一个用于表示迁移资源消耗的迁移回报结构N：S×A×S→R≥0后构成的。

模型中，若P（s1，a，n，s2）＝0.5，则表示在s1与s2存在一个动作a的迁移，发生迁移的概率为0.5，迁出s1状态的迁移资源消耗为n。

2 模型MTBDD表示

OBDD作为化简了的二元决策图，是一个具有1个根节点和2个终端结点 （标记为0和1）的有向无环图，使用OBDD验证模型的基本思想是通过蕴含的办法，用OBDD来表示模型检测中转移关系、可达状态集合，以此来进行不动点的计算［9］，OBDD的使用使得现有的模型检测器可以对状态数高达10120的系统进行验证［10］。

多终 端 二 元 决 策 图 （multi－terminal binary decision diagrams，MTBDD）扩展了OBDD的表示范围，可以用来表示一个从多维布尔值域到任意实数集的函数f（v1，v2，…vn）：｛0，1｝n→R，因其终端结点可以有多个并且可以是任意实数，因此可通过终端结点来表示随机系统模型的不同迁移概率、迁移离开率等信息，进而进行随机系统模型的分析验证。

例1 随机系统模型MTBDD举例

图1表示一个由4个状态构成的DTMC，其状态迁移MTBDD表示如图2所示。

对于传统的MTBDD，本文通过以下的方法进行改进：将终端节点的取值范围集合由实数集变改为实数对偶集，从而使这种多终端二元决策图可用来表示任一从多维布尔值域到任意实数对偶集合的函数f（v1，v2，…vn）：｛0，1｝n→（R∈［0，1］，R＇≥0），其中实数对偶分别用来表示随机系统模型的迁移概率及迁移资源消耗。

图1 DTMC模型举例

图2 DTMC模型MTBDD表示

3 DTMRDP模型对称约减

对于本文描述的DTMRDP模型，由于在状态迁移过程中，伴随着多种复杂特征信息，因此其对称约减方法有别于一般的非概率迁移系统。

定义3 自同构

若迁移系统M＝（S，R），其中S为状态的有限集，迁移关系RS×S，则状态空间S上的自同构表示为π：S→S，且满足：如果 （s，s＇）∈R ，则 （π（s），π（s＇））∈R 。

定义4 等价关系

对于给定的一组自同构G，状态空间S的等价关系θ表示为 （s，π（s））∈θ。

定义5 迁移系统商

设迁移系统M＝（S，R），对于状态空间的每一个等价类，通过引入迁移关系珚R＝｛（rep（s），rep（s，s＇）∈R｝及等价类状态唯一表示函数rep：S→珚S，可构造出原迁移系统的商，表示为珨M＝（珚S，珚R）。对于M＝（S，R）而言，因为自同构保留了迁移关系R，所以迁移系统商珨M与原迁移系统M等价互模拟。

对于前文中提到的DTMC、DTMRDP模型，约减后的商模型定义如下：

定义6 DTMC商模型

定义7 DTMRDP商模型

若DTMRDP模型M ＝ （S，P，A，N），则其商模型表示为＝），对于所有状态s，商模型状态迁移概率及迁移回报计算方法如下

在DTMC及DTMRDP商模型的定义中，由于标记函数、原子命题、初始状态与商模型构造无关，所以在商模型构造中并未对它们进行具体说明。

例2 DTMRDP模型对称约减示例

本例修改使用了文献 ［8］中的对称进程实例，假设存在两个对称的进程，每个进程有三个状态 （0、1和2），且两个进程在进行状态变迁时除了满足一定的随机性以外，同时还会消耗数量为n的资源，这样的两个对称进程的工作状态变迁可由DTMRDP模型表示。

设最初两个进程都处于状态0，进程的工作时序如下：第一步，两个进程中的任一个均可以以概率0.5随机地移动到状态1或2；第二步：在第一步中未发生状态变化的进程随机地移动到状态1或2，但要求若该步中某一进程移动到状态2，则另一进程在此步骤须移动到状态1。

本例可通过图3所示的DTMRDP模型进行描述，由于假设各状态在发生状态变迁时的动作相同，故在图3中省略了动作描述。

通过图4中给出的等价关系唯一表示函数，可以对原模型中的状态集进行约减，借助于本文后面提出的迁移关系对称约减算法将得出如图5所示的对称约减商DTMRDP模型，模型的状态个数及迁移个数明显减少。

图3 对称进程DTMRDP模型

图4 等价关系唯一表示函数

4 算法描述

图5 对称约减商DTMRDP模型

对于DTMRDP模型的对称约减过程，下面给出基于原模型状态迁移矩阵的对称约减算法，其转换过程大致可以分为矩阵行消除、矩阵列累加和规一化处理等几步，相应的算法描述如下：

状态迁移矩阵的对称约减算法：

本算法基本操作为矩阵运算，算法复杂性不高，由于篇幅原因，本文不做具体分析。

5 实例说明

对于图3所示的对称进程DTMRDP模型，该模型的迁移矩阵MTBDD表示如图6所示。

依据本文提出的算法，相应的模型迁移矩阵对称约减转换过程见图7（a）至图7（d）。

得出模型约减后的状态迁移MTBDD表示如图8所示，可见原模型中的状态集及迁移关系均被大大缩减。

图6 约减前状态迁移MTBDD表示

图7 迁移矩阵对称约减算法实例说明

图8 约减后状态迁移MTBDD表示

6 结束语

本文借鉴了传统的符号模型检测技术，改进了二元决策图的表示形式，将符号模型检测技术和对称约减技术综合应用于复杂概率模型，基于迁移矩阵提出了相应的约减方法并给出了算法描述，通过实例证明了该方法的有效性，缩减了模型的状态空间，提高了随机系统模型的验证规模，扩大了模型检测的应用范围。下一步作者将进一步研究其它概率模型的约减处理方法，并对现实系统的应用进行深入分析。

［1］Marta Kwiatkowska，Gethin Norman，David Parker.Advances and challenges of probabilistic model checking ［C］／／Proceedings of the 48th Annual Allerton Conference on Communication，Control and Computing.2010：1691－1698.

［2］WU Lijun，SU Jinshu，SU Kaile.Symbolic model checking knowledge and time in multi－agent system via extended mu－calculus［J］.Chinese Journal of Computers，2008 （2）：245－252（in Chinese）.［吴立军，苏金树，苏开乐.多智能体系统时态认知规范高效符号模型检测的算法研究 ［J］.计算机学报，2008 （2）：245－252.］

［3］MA Yanan，LIU Nan，ZHU Yuefei，et al.Stuttering partial－order reduction algorithm in verification of security protocols ［J］.Application Research of Computers，2011 （9）：3488－3491 （in Chinese）.［马亚南，刘楠，祝跃飞，等.安全协议状态空间的束动作偏序约简算法 ［J］.计算机应用研究，2011 （9）：3488－3491.］

［4］ZHOU Conghua，LIU Zhifeng，WANG Changda.Bounded model checking for probabilistic computation tree logic ［J］.Journal of Software，2012，23 （7）：1665－1668 （inChinese）.［周从华，刘志锋，王昌达.概率计算树逻辑的限界模型检测［J］.软件学报，2012，23（7）：1665－1668.］

［5］NIU Jun，ZENG Guosun，WANG Wei.An approach of model checking time or space performance ［J］.Chinese Journal of Computers，2010，33 （9）：1621－1633（in Chinese）. ［钮俊，曾国荪，王伟.基于模型检测的时间空间性能验证方法 ［J］.计算机学报，2010，33 （9）：1621－1633.］

［6］Jaghoori M M，Sirjani M，Mousavi M R，et al.Symmetry and partial order reduction techniques in model checking rebeca ［J］.Acta Informatica，2010 （47）：33－66.

［7］Donaldson A F，Miller A，Parker D.Language level symmetry reduction for probabilistic model checking ［C］／／Proceedings of the Sixth International Conference on the Quantitative Evaluation of Systems.Washington DC，USA：IEEE Computer Society，2009：289－298.

［8］Marta Kwiatkowska，Gethin Norman，David Parker.Symmetry reduction for probabilistic model checking ［C］／／Proceedings of the 18th International Conference on Computer Aided Verification.Seattle，United States：Springer－Verlag，2006：7－20.

［9］YAO Quanzhu，WEI Xiaoyong.Improved algorithm of PRE■operation in symbolic model checking based on OBDD ［J］.Computer Engineering，2008（14）：69－71 （in Chinese）.［姚全珠，魏小勇.基于OBDD的SMC中PRE■操作的改进算法［J］.计算机工程，2008（14）：69－71.］

［10］Clarke E M，Emerson E A，Sifakis J.Model checking：Algorithmic verification and debugging ［J］.Communications of the ACM 2009，52（11）：74－84.