Abstract:

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.

Key words: computation tree logic(CTL), model checking, binary decision diagram(BDD)

摘要： 在计算树逻辑(CTL)中引入过去时态算子，得到了表达力更强的属性规约语言CTLP，给出了CTLP 的模型检测算法及其固定点刻画。该算法的复杂性和CTL一样。固定点刻画使得CTLP的符号模型检测过程能够实现，从而有效克服了模型检测中的状态爆炸问题。

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

CLC Number: 

• TP311.5