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

摘要：

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

关键词： 模型检测 时段演算 Kripke结构 逻辑CTL NP完全问题 逻辑运算符 验证问题

作者: 梁爱丽 朱嘉奇 王捍贫 屈婉玲

作者单位: 北京大学信息科学技术学院软件研究所可信软件技术教育部重点实验室,北京,100871

会议类型: 国内会议

会议名称: 2007全国理论计算机科学学术年会

会议地点: 南宁

会议语种:中文

页码: 169-174

在线出版日期: 2007-11-01（万方平台首次上网日期，不代表论文的发表时间）