符号化模型检测CTL

• 作者: 吕关锋 苏开乐 骆翔宇
• 来源期刊: 计算机学报
• 学科: 工学
• 关键词: 模型检测 时态逻辑 有序二值判定图(OBDD)
• 年，卷（期）: 2005,（11）
• 所属期刊栏目: 研究论文与技术报告
• 页码范围: 1798-1806
• 页数: 9页
• 分类号: TP301
• 字数: 7663字
• 语种: 中文
• DOI: 10.3321/j.issn:0254-4164.2005.11.005

摘要

提出了一个关于时态逻辑CTL* 的符号化模型检测算法.该算法通过所谓的tableau构造方法来判定一个有限状态系统是否满足CTL*规范. 根据该理论,作者已实现了一个基于OBDD技术的CTL*符号化模型检测工具MCTK,并完成了相当数量的实验.到目前为止,已知有名的符号化模型检测工具,如SMV和NuSMV等, 都只能对CTL*的子集逻辑(如CTL,LTL)进行检测,而文中算法的结果是令人满意的,并且当规范不是特别复杂时, 高效的CTL*符号化模型检测是可能的.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	苏开乐	中山大学计算机科学系	22	309	11.0	17.0
3	吕关锋	北京工业大学计算机科学与技术学院	7	113	4.0	7.0
6	骆翔宇	中山大学计算机科学系	3	110	3.0	3.0