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

Symmetry reduction method for complicated system model based on decision diagrams

作　　者：纪明宇[1,2] 王海涛[1] 陈志远[2] 李艳梅[2] 

机构地区：[1]东北林业大学信息与计算机工程学院,黑龙江哈尔滨150040 [2]哈尔滨工程大学计算机科学与技术学院,黑龙江哈尔滨150001

出　　处：《计算机工程与设计》2013年第10期3685-3689,共5页Computer Engineering and Design

基　　金：中央高校基本科研业务费专项基金项目(DL11BB08);国家自然科学基金项目(71001023)

摘　　要：针对复杂随机系统模型检测过程中的状态空间爆炸问题,提出一种用于支持迁移回报特征描述的概率模型对称约减方法。通过引入状态集等价关系唯一表示函数,约减了原模型中的状态集尺寸;通过加入回报特征描述,改进了传统的多终端二元决策图,用于表示概率回报模型中的迁移关系;基于迁移矩阵,提出了一种高效的对称约减算法,完成了迁移关系的约简。实验结果表明了该方法的可行性与有效性。To solve the state space explosion problem of model checking process for complicated stochastic systems,a symmetry reduction method based probabilistic model which supports the transition reward characteristics is proposed.The size of the state set in the original model is decreased by using the exclusive representation function of the state set equivalence relations and the traditional multi-terminal binary decision diagram is improved by adding the return characteristics which is used to represent the transition relations of probabilistic reward model,an efficient symmetric reduction algorithm is proposed for reduce transition relations based on transition matrix.The example result shows the feasibility and validity of the method.

关 键 词：形式化验证 模型检测 状态空间爆炸 决策图 对称约减 商模型 

分 类 号：TP302.7[自动化与计算机技术—计算机系统结构]