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

• 作者: 屈婉玲 朱嘉奇 梁爱丽 王捍贫
• 来源期刊: 计算机研究与发展
• 学科: 工学
• 关键词: 模型检测 CTL* QDDC NP-完全
• 年，卷（期）: 2008,（z1）
• 所属期刊栏目: 数据、程序及其理论
• 页码范围: 169-174
• 页数: 6页
• 分类号: TP301
• 字数: 5322字
• 语种: 中文

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	屈婉玲	北京大学信息科学技术学院软件研究所可信软件技术教育部重点实验室	10	168	6.0	10.0
2	王捍贫	北京大学信息科学技术学院软件研究所可信软件技术教育部重点实验室	14	23	3.0	4.0
3	梁爱丽	北京大学信息科学技术学院软件研究所可信软件技术教育部重点实验室	1	3	1.0	1.0
4	朱嘉奇	北京大学信息科学技术学院软件研究所可信软件技术教育部重点实验室	1	3	1.0	1.0