一种优化的可能性测度计算树逻辑检测模型

作     者：陈燕升 张赞波 吴忠坤 任江涛 CHEN Yansheng;ZHANG Zanbo;WU Zhongkun;REN Jiangtao

作者机构：广东轻工职业技术学院环境工程系广东广州510300 昆山科技大学资讯管理系台湾台南71003 广东轻工职业技术学院计算机工程系广东广州510300 中山大学软件学院广东广州510275 

出 版 物：《中山大学学报（自然科学版）》 (Acta Scientiarum Naturalium Universitatis Sunyatseni)

年 卷 期：2015年第54卷第4期

页      面：49-54页

核心收录：

学科分类：08[工学] 081202[工学-计算机软件与理论] 0812[工学-计算机科学与技术（可授工学、理学学位）] 

基　　金：国家自然科学基金资助项目(11471342) 广东省教育科研"十二五"规划2012年度研究资助项目(2012JK089) 广东省高职教育教改资助项目(201401034) 校级自然科学基金资助项目(KJ201311/KJ2014) 

主　　题：可能性测度 模型检测 公共子表达式 计算树逻辑 

摘      要：可能性测度计算树逻辑模型检测验证中存在诸多问题,例如低性能效率和高时间复杂度。针对上述问题,基于传统的模型检测标记算法,为满足高复杂性、大规模的公式标记检测,设计并实现了I-PM_CTL算法。其基本步骤如下:第一步,先利用相关可能性测度对逻辑树公式进行计算,预处理标识公共子表达式的唯一性;第二步,在充分确保模型检测空间平衡状态下设定公共子表达式与可能性测度计算树逻辑模型状态;第三步,实施验证,为可能性测度计算树逻辑公式以极大概率一次性实现验证提供了保证。经过模拟实验发现,这一种方法一方面在很大程度上减小了相关时间复杂度,另一方面还使验证性能有所提升。