具有过去时态算子的计算树逻辑模型检测  

Model Checking of Computation Tree Logic with Past Temporal Operators

作　　者：周从华[1] 刘志锋[1] 

机构地区：[1]江苏大学计算机科学与通信工程学院,镇江212013

出　　处：《计算机工程》2007年第22期98-100,共3页Computer Engineering

基　　金：国家自然科学基金资助项目(60573046)

摘　　要：在计算树逻辑(CTL)中引入过去时态算子,得到了表达力更强的属性规约语言CTLP,给出了CTLP的模型检测算法及其固定点刻画。该算法的复杂性和CTL一样。固定点刻画使得CTLP的符号模型检测过程能够实现,从而有效克服了模型检测中的状态爆炸问题。This paper introduces the past temporal operators into computation tree logic（CTL）, and obtains a new specification language CTLP which is more expressive than CTL. CTLP model checking algorithm is proposed and its time complexity is the same as CTL. The fixpoint representation of CTLP is presented which makes CTLP model checking symbolic. The symbolic algorithm can overcome the state explosion problem efficiently in model checking.

关 键 词：计算树逻辑 模型检测 二叉判定图 

分 类 号：TP311.5[自动化与计算机技术—计算机软件与理论]