概率计算树逻辑的限界模型检测

• 作者: 刘志锋 周从华 王昌达
• 来源期刊: 软件学报
• 学科: 工学
• 关键词: 模型检测 限界模型检测 概率计算树逻辑 马尔可夫链
• 年，卷（期）: 2012,（7）
• 所属期刊栏目: 理论计算机科学
• 页码范围: 1656-1668
• 分类号: TP301
• 字数: 11576字
• 语种: 中文
• DOI: 10.3724/SP.J.1001.2012.04089

摘要

为了缓解概率计算树逻辑模型检测中的状态空间爆炸问题,提出了概率计算树逻辑的限界模型检测技术.该技术首先定义概率计算树逻辑的限界语义,并证明其正确性；之后,通过实例说明在传统限界模型检测中,以路径长度作为判断检测过程终止的标准已经失效,基于数值计算中牛顿迭代法的终止准则,设计了新的终止判断标准;然后提出基于线性方程组求解的限界模型检测算法；最后,通过3个测试用例说明,概率计算树逻辑限界模型检测方法在反例较短的情况下能够快速完成检测过程,而且比概率计算树逻辑的无界模型检测算法所需求得的状态空间要少.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	王昌达	江苏大学计算机科学与通信工程学院	50	237	9.0	13.0
2	周从华	江苏大学计算机科学与通信工程学院	46	193	7.0	11.0
3	刘志锋	江苏大学计算机科学与通信工程学院	29	118	5.0	10.0