一种新的时段演算及其验证  

A New Duration Calculus and Its Verification

作　　者：梁爱丽[1] 朱嘉奇[1] 王捍贫[1] 屈婉玲[1] 

机构地区：[1]北京大学信息科学技术学院软件研究所可信软件技术教育部重点实验室,北京100871

出　　处：《计算机研究与发展》2008年第z1期169-174,共6页Journal of Computer Research and Development

基　　金：国家"九七三"重点基础研究发展规划基金项目(2002CB312004);国家"八六三"高技术研究发展计划基金项目(2006AA01Z160)

摘　　要：在Pandya提出的CTL*[DC]逻辑的基础上,对其语法和语义进行扩展,并对路径长度进行限制,定义了一个新的逻辑CTL*[k-QDDC],它可应用于实时系统的描述和验证.给出了在Kripke结构中直接验证CTL*[k-QDDC]逻辑公式在某状态是否成真的基本算法.在某些假设下,也证明了CTL*[k-QDDC]中的某个逻辑运算符的验证问题是NP完全的,这就说明CTL*[k-QDDC]的验证问题至少是NP难的.Based on the logic CTL*[DC] proposed by Pandya, we extend its syntax and semantics, and restrict the length of the path, to define a new logic CTL*[k-QDDC], which can be applied to describe and verify real-time systems. We propose a basic algorithm verifying directly whether a formula of logic CTL*[k-QDDC] is true for a state in Kripke structure. We also show that under some assumptions, the verification of a logical operator of CTL*[k-QDDC] is NP-complete, which suggests that the whole verification problem is at least NP-hard.

关 键 词：模型检测 CTL* QDDC NP-完全 

分 类 号：TP301[自动化与计算机技术—计算机系统结构]