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

作者：周从华; 邢支虎; 刘志锋; 王昌达

来源：计算机学报, 2013, (12): 2587-2600.

• 模型检测
• 限界模型检测
• 概率计算树逻辑
• 马尔可夫决策过程
• 状态空间爆炸 model checking
• bounded model checking
• probabilistic computation tree logic
• Markov decision processes
• state space explosion

限界模型检测避免了符号模型检测反应式系统中构建二叉图时出现的空间快速增长,已经被证明是缓解状态空间爆炸问题的有力技术.文中遵循限界模型检测的思想,对马尔可夫决策过程提出一种限界模型检测技术,从而避免构建多端二叉图时空间的快速增长.具有非确定选择刻画能力是马尔可夫决策过程最大的特性,针对该特性首先定义概率计算树逻辑的限界语义,并证明其正确性;然后基于不同界下所计算概率度量序列的演化趋势,设计了限界检测过程终止的判断准则;最后将限界模型检测过程转换为线性方程组的求解问题.实验结果说明限界模型检测技术在证据较短的情况下,所需内存空间少于无界模型检测算法.

• 出版日期2013
• 单位江苏大学