《计算机学报》文章摘要   全文下载
文章题目	符号化模型检测CTL*
作者	苏开乐1),2) 骆翔宇1) 吕关锋3)
作者单位	1)(中山大学计算机科学系 广州 510275) 2)(河南科技大学电子信息工程学院 洛阳 471003) 3)(北京工业大学计算机科学与技术学院 北京 100022)
发表年份	2005
发表月份	11期(1798—1806)
文章摘要	摘要 提出了一个关于时态逻辑CTL*的符号化模型检测算法.该算法通过所谓的tableau构造方法来判定一个有限状态系统是否满足CTL*规范.根据该理论,作者已实现了一个基于OBDD技术的CTL*符号化模型检测工具MCTK,并完成了相当数量的实验.到目前为止,已知有名的符号化模型检测工具,如SMV和NuSMV等,都只能对CTL*的子集逻辑(如CTL,LTL)进行检测，而文中算法的结果是令人满意的,并且当规范不是特别复杂时,高效的CTL*符号化模型检测是可能的. 关键词 模型检测;时态逻辑;有序二值判定图(OBDD) 中图法分类号 TP301