计算树逻辑特性模式研究

摘要：

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

关键词：计算树逻辑、特性模式、模型检查

所属期刊栏目：35

分类号：TP311(计算技术、计算机技术)

在线出版日期：2010-03-02（万方平台首次上网日期，不代表论文的发表时间）

页数：共3页

页码：68-70