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

The Model of Checking Method Based on Improved Computation Tree Logic Possibility Measure

作　　者：陈燕升[1,2] 张赞波[3] 吴忠坤[3] 任江涛[4] 

机构地区：[1]广东轻工职业技术学院环境工程系,广东广州510300 [2]昆山科技大学资讯管理系,台湾台南71003 [3]广东轻工职业技术学院计算机工程系,广东广州510300 [4]中山大学软件学院,广东广州510275

出　　处：《中山大学学报（自然科学版）》2015年第4期49-54,共6页Acta Scientiarum Naturalium Universitatis Sunyatseni

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

摘　　要：可能性测度计算树逻辑模型检测验证中存在诸多问题,例如低性能效率和高时间复杂度。针对上述问题,基于传统的模型检测标记算法,为满足高复杂性、大规模的公式标记检测,设计并实现了I-PM_CTL算法。其基本步骤如下:第一步,先利用相关可能性测度对逻辑树公式进行计算,预处理标识公共子表达式的唯一性;第二步,在充分确保模型检测空间平衡状态下设定公共子表达式与可能性测度计算树逻辑模型状态;第三步,实施验证,为可能性测度计算树逻辑公式以极大概率一次性实现验证提供了保证。经过模拟实验发现,这一种方法一方面在很大程度上减小了相关时间复杂度,另一方面还使验证性能有所提升。To settle various problems in computation tree logic possibility measure model validation process,such as high time complexity and low efficiency performance. The I-PM_ CTL algorithm is proposed. The algorithm is based on the traditional model checking mark algorithm,so that it is adaptable to the need of mark detection of large-scale,highly complex formulas. The steps of the algorithm are as follows. Fristly,the logic tree formulas are calculated using relevant possibility measure,which is a preprocessing step to identify the uniqueness of the common sub-expressions. Secondly,it specifies the state of common sub-expressions and I-PM_ CTL model,while maintaining the equilibrium of model checking space. Finally,this algorithm implements the verification,ensuring the I-PM_ CTL formulas verification to be completed in one time with high probability. The results of simulation experiments show that the I-PM_ CTL algorithm not only effectively reduces time complexity,but also improves the verification performance.

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

分 类 号：TP301.2[自动化与计算机技术—计算机系统结构]