马尔可夫决策过程的限界模型检测  

Bounded Model Checking for Markov Decision Processes

作　　者：周从华[1] 邢支虎 刘志锋[1] 王昌达[1] 

机构地区：[1]江苏大学计算机科学与通信工程学院,江苏镇江212013

出　　处：《计算机学报》2013年第12期2587-2600,共14页Chinese Journal of Computers

基　　金：国家自然科学基金青年基金(61300228;61003288);中德合作交流基金(6111130184);江苏省自然科学基金(BK2010192);教育部博士点基金(20093227110005)资助~~

摘　　要：限界模型检测避免了符号模型检测反应式系统中构建二叉图时出现的空间快速增长,已经被证明是缓解状态空间爆炸问题的有力技术.文中遵循限界模型检测的思想,对马尔可夫决策过程提出一种限界模型检测技术,从而避免构建多端二叉图时空间的快速增长.具有非确定选择刻画能力是马尔可夫决策过程最大的特性,针对该特性首先定义概率计算树逻辑的限界语义,并证明其正确性;然后基于不同界下所计算概率度量序列的演化趋势,设计了限界检测过程终止的判断准则;最后将限界模型检测过程转换为线性方程组的求解问题.实验结果说明限界模型检测技术在证据较短的情况下,所需内存空间少于无界模型检测算法.Bounded model checking has been proven to be a powerful technique for the verification of reactive systems, since it can avoid the space blow up of BDDs（Binary Decision Diagrams）. To avoid the space blow up of MTBDDs （Multi Terminal Binary Decision Diagrams）, a bounded model checking technique for Markov decision processes is proposed. The biggest feature of Markov decision processes is able to describe the nondeterministic choice. For this feature, the bounded semantics of the probabilistic computation tree logic is first presented, and its correct- ness is proven. Second, based on the evolution trend of the sequence consisting of probability measure calculated by the bounded model checking procedure, three termination criterions are given. Third, the bounded model checking procedure of the probabilistic computation tree logic is transformed into a linear equation. Finally, the experiment results show that compared with the unbounded model checking if the length of the witness is short then the bounded model checking needs less space.

关 键 词：模型检测 限界模型检测 概率计算树逻辑 马尔可夫决策过程 状态空间爆炸 

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