Abstract: Model checking is an effective method for system verification and validation. Temporal logic formulas are used to specify system properties to be verified and verified in a model checking tool. This paper introduces the syntax and semantics of Computation Tree Logic(CTL), presents property patterns of CTL based on the partition and scope of CTL, which includes absence model, absence model, university model, precedence model, response model, and so on.

Key words: Computation Tree Logic(CTL), property patterns, model checking

摘要： 模型检查是系统验证的有效方法，在验证过程中需要对系统待检验特性用时态逻辑公式进行刻画，然后在模型检查工具中进行检验。介绍计算树逻辑的语法及语义，根据计算树逻辑中特性模式的划分及作用范围给出计算树逻辑常见的特性模式，包括缺失性模式、存在性模式、普遍性模式、优先性模式和跟随性模式等。

关键词: 计算树逻辑, 特性模式, 模型检查

CLC Number: 

• TP311