广义可能性决策过程的计算树逻辑模型检测

摘要：

模型检测作为一种形式化验证技术,已被广泛应用于各种并发系统的正确性验证.针对具有非确定性选择和广义可能性分布的并发系统,引入广义可能性决策过程作为此类系统的模型;给出描述其性质的规范语言广义可能性计算树逻辑的概念;研究此类系统的广义可能性计算树逻辑模型检测问题.结论表明,其模型检测算法的时间复杂度也为多项式时间.所获得的结果扩大了广义可能性测度在模型检测中的应用范围.

关键词： 计算树逻辑 模型检测算法 时间复杂度

作者: 马占有 李永明

作者单位: 陕西师范大学计算机科学学院 陕西西安710062;北方民族大学计算机科学与工程学院 宁夏银川750021 陕西师范大学计算机科学学院 陕西西安710062

会议类型: 国内会议

会议名称: 2015全国理论计算机科学学术年会

会议地点: 金华

会议语种:中文

页码: 1-7

在线出版日期: 2015-10-30（万方平台首次上网日期，不代表论文的发表时间）