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

Model Checking of Computation Tree Logic with Past Temporal Operators

在计算树逻辑(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.