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

（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）为初始分布集合。……