|
|||||
|
|
| 符号化模型检测CTL | |
| 引用本文： | 苏开乐,骆翔宇,吕关锋.符号化模型检测CTL[J].计算机学报,2005,28(11):1798-1806. |
| 作者姓名： | 苏开乐 骆翔宇 吕关锋 |
| 作者单位： | 1. 中山大学计算机科学系,广州,510275;河南科技大学电子信息工程学院,洛阳,471003 2. 中山大学计算机科学系,广州,510275 3. 北京工业大学计算机科学与技术学院,北京,100022 |
| 基金项目： | 本课题得到国家自然科学基金（60496327, 10410638, 60473004）;广东省自然科学基金团队项目（04205407）与教育部留学回国人员科研启动基金以及上海市智能信息处理重点实验室（筹）开放课题资助. |
| 摘 要： | 提出了一个关于时态逻辑CTL＊ 的符号化模型检测算法.该算法通过所谓的tableau构造方法来判定一个有限状态系统是否满足CTL＊规范. 根据该理论,作者已实现了一个基于OBDD技术的CTL＊符号化模型检测工具MCTK,并完成了相当数量的实验.到目前为止,已知有名的符号化模型检测工具,如SMV和NuSMV等, 都只能对CTL＊的子集逻辑（如CTL,LTL）进行检测,而文中算法的结果是令人满意的,并且当规范不是特别复杂时, 高效的CTL＊符号化模型检测是可能的. |
| 关 键 词： | 模型检测 时态逻辑 有序二值判定图（OBDD） |
| 收稿时间： | 2004-08-29 |
| 修稿时间： | 2004-08-292005-07-14 |
Symbolic Model Checking for CTL |
|
| SU Kai-Le,LUO Xiang-Yu,LU Guan-Feng.Symbolic Model Checking for CTL[J].Chinese Journal of Computers,2005,28(11):1798-1806. | |
| Authors: | SU Kai-Le LUO Xiang-Yu LU Guan-Feng |
| Affiliation: | 1.Department of Computer Science, Sun Yat-Sen University, Guangzhou 510275; 2. Institute of Electronics and Information Engineering, Henan University of Science and Technology, Luoyang 471003; 3.College of Computer Science and Technology, Beijing University of Technology, Beijing 100022 |
| Abstract: | This paper gives a symbolic model checking algorithm for the temporal logic CTL~*.The algorithm determines whether a finite state system satisfies a formula in CTL~* using the method of symbolic(tableau) construction.According to our algorithm,we had implemented a new CTL~* symbolic model checker(MCTK) by means of OBDD and obtained some experimental results.Up to now,the well-known symbolic model checking tools(SMV,NuSMV etc.) have been implemented only for the sublogics of CTL~*,such as CTL and LTL.The results that we have obtained in this paper are quite surprising and show that efficient CTL~* model checking is possible when the specifications are not excessively complicated. |
| Keywords: | model checking temporal logic Ordered Binary Decision Diagrams(OBDD) |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ | |