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

计算机科学 ›› 2013, Vol. 40 ›› Issue (10): 122-126.

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

奚琪,王清贤,曾勇军,秦艳锋

国家数字交换系统工程技术研究中心郑州450002;国家数字交换系统工程技术研究中心郑州450002;国家数字交换系统工程技术研究中心郑州450002;国家数字交换系统工程技术研究中心郑州450002

出版日期:2018-11-16 发布日期:2018-11-16
基金资助:
本文受国家863计划(2012AA012902)资助

Improved Algorithm for Large-scale CTL Formulae Verification

XI Qi,WANG Qing-xian,ZENG Yong-jun and QIN Yan-feng

Online:2018-11-16 Published:2018-11-16

摘要/Abstract

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

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

Abstract: Labelling algorithm is a standard algorithm for model checking CTL formulas．This paper presented an algorithm 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 results illustrate the advantages on the efficiency of the new algorithm．

Key words: Model checking,Labelling algorithm,Common subformulas,Parse tree

奚琪,王清贤,曾勇军,秦艳锋. 一种改进的大规模CTL公式检测算法[J]. 计算机科学, 2013, 40(10): 122-126. https://doi.org/

XI Qi,WANG Qing-xian,ZENG Yong-jun and QIN Yan-feng. Improved Algorithm for Large-scale CTL Formulae Verification[J]. Computer Science, 2013, 40(10): 122-126. https://doi.org/

参考文献

[1] Clarke E,Grumberg O,Peled D．Model Checking(Second Prin-ting)[M]．London:MIT Press,2000:27-30
[2] Michael H,Maark R．Logic In Computer Science:Modelling and Resoning about System(Second Edition)[M]．London:Combridge University Press,2004:221-229
[3] Clarke E,Emerson E,Sistla A．Automatic Verification of Finite-State Concurrent Systems Using Temporal Logic Specifcations[C]∥ACM Transactions on Programming Languages and Systems．1986,8:244-263
[4] Vergauwen B,Lewi J．A Linear Local Model Checking Algorithm for CTL[C]∥Proceedings of 4^th International Conference on Concurrency Theory,1993.Hidesheim,Germany,Springer-Verlag,1993:447-461
[5] Heljanko K．Implementing a CTL Model checker[C]∥Workshop Concurrency:Specification & Programming．Humboldt-University zu Berlin, Institut fur Informatik,1996:75-84
[6] Mumme M,Ciardo G．A fully symbolic bisimulation algorithm[C]∥Giorgio Delzanno and Igor Potapov．RP,volume 6945of Lecture Notes in Computer Science,Springer,2011:218-230
[7] Lefticaru R,Ipate F．Automated Model Design using Genetic Algorithms and Model Checking[C]∥2009Fourth Balkan Confe-rence in Informatics(BCI’09)．Thessaloniki,IEEE Computer Society,2009:79-84
[8] 李梦君,李舟军,陈火旺．基于抽象解释理论的程序验证技术[J]．软件学报,2008,9(1):17-26
[9] Cousot P．Formal Verification by Abstract Interpretation[C]∥NASA Formal Methods 2012,4th International Symposium．NFM,Norfolk,VA,USA,2012:3-7
[10] Meulen J V,Pecheur C．Milestones:A model checker combining symbolic model checking and partial order reduction[C]∥NASA Formal Methods 2011,volume 6617of LNCS．Springer,2011:525-531

Metrics

Viewed

Full text

Abstract

Cited

Shared

Discussed