中山大学学报（自然科学版）Issue(4)：49-54,6.DOI:10.13471/j.cnki.acta.snus.2015.04.009
一种优化的可能性测度计算树逻辑检测模型
The Model of Checking Method Based on Improved Computation Tree Logic Possibility Measure
摘要
Abstract
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 pro-posed.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 fol-lows.Fristly,the logic tree formulas are calculated using relevant possibility measure,which is a prepro-cessing 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 per-formance.关键词
可能性测度/模型检测/公共子表达式/计算树逻辑Key words
possibility measure/model checking/common sub-expression/computation tree logic分类
信息技术与安全科学引用本文复制引用
陈燕升,张赞波,吴忠坤,任江涛..一种优化的可能性测度计算树逻辑检测模型[J].中山大学学报（自然科学版）,2015,(4):49-54,6.基金项目
国家自然科学基金资助项目（11471342）；广东省教育科研“十二五”规划2012年度研究资助项目（2012JK089）；广东省高职教育教改资助项目（201401034）；校级自然科学基金资助项目 （）
