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

Improved Algorithm for Large-scale CTL Formulae Verification

作　　者：奚琪[1] 王清贤[1] 曾勇军[1] 秦艳锋[1] 

机构地区：[1]国家数字交换系统工程技术研究中心,郑州450002

出　　处：《计算机科学》2013年第10期122-126,共5页Computer Science

基　　金：国家863计划(2012AA012902)资助

摘　　要：标记算法是模型检测用于验证计算树逻辑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.

关 键 词：模型检测 标记算法 公共子公式 语法分析树 

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