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

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

可能性测度计算树逻辑模型检测验证中存在诸多问题,例如低性能效率和高时间复杂度。针对上述问题,基于传统的模型检测标记算法,为满足高复杂性、大规模的公式标记检测,设计并实现了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.