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

来源：计算机工程与科学杂志2015年第11期北京时间：

作者：马占有1，2，李永明1

单位：1.陕西师范大学计算机科学学院，陕西 西安 710062；2.北方民族大学计算机科学与工程学院，宁夏 银川 750021

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

关键词：并发系统,广义可能性决策过程,广义可能性计算树逻辑,模型检测,

基金资助：国家自然科学基金资助项目(11271237,61228305,61462001);北方民族大学资助项目(2014XB213)