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

作     者：梁爱丽 朱嘉奇 王捍贫 屈婉玲 Liang Aili;Zhu Jiaqi;Wang Hanpin;Qu Wanling

作者机构：北京大学信息科学技术学院软件研究所可信软件技术教育部重点实验室北京100871 

出 版 物：《计算机研究与发展》 (Journal of Computer Research and Development)

年 卷 期：2008年第45卷第Z1期

页      面：169-174页

核心收录：

学科分类：08[工学] 081202[工学-计算机软件与理论] 0812[工学-计算机科学与技术（可授工学、理学学位）] 

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

主　　题：模型检测 CTL* QDDC NP-完全 

摘      要：在Pandya提出的CTL*[DC]逻辑的基础上,对其语法和语义进行扩展,并对路径长度进行限制,定义了一个新的逻辑CTL*[k-QDDC],它可应用于实时系统的描述和验证.给出了在Kripke结构中直接验证CTL*[k-QDDC]逻辑公式在某状态是否成真的基本算法.在某些假设下,也证明了CTL*[k-QDDC]中的某个逻辑运算符的验证问题是NP完全的,这就说明CTL*[k-QDDC]的验证问题至少是NP难的.