一种改进的大规模CTL公式检测算法

Improved Algorithm for Large-scale CTL Formulae Verification

标记算法是模型检测用于验证计算树逻辑CTL公式的经典算法。针对标记算法检测大规模公式存在的效率问题,提出一种可用于验证大规模CTL公式的标记算法。算法通过公式预处理标识公式集中的公共子公式,在验证过程中绑定公共子公式与模型状态,避免公式的重复验证。实验结果表明,该算法有效提高了验证效率。

Labelling algorithm is a standard algorithm for model checking CTL formulas. This paper presented an algo-rithm to improve efficiency for large-scale CTL formulas verification. It identifies common subformulas from formulae set,binding program states with labels of common subformulas to avoid repeating checking them. The experimental re-sults illustrate the advantages on the efficiency of the new algorithm.