| 结合搜索空间划分和抽象进行LTL模型检测 |
| 蒲飞; 张文辉
|
| 2007
|
| 发表期刊 | 中国科学E辑
 |
| ISSN | 1006-9275
|
| 卷号 | 37期号:12页码:1504-1520 |
| 摘要 | 在应用模型检测于工业系统时, 状态空间爆炸仍然是一个主要的障碍. 基于抽象的方法在克服状态空间爆炸方面取得了很大的成功. 提出一种结合搜索空间划分和抽象的方法来降低模型检测的空间复杂度. 划分依赖于每个所分划的搜索空间的表达. 特别地, 划分可以逐步求精以获得更好的空间消减. 从数值实验看, 这种搜索空间划分和抽象的结合在基于内存的需求上能提高验证的效率, 同时能得到比单独使用其中一种方法更好的效果. |
| 关键词 | 搜索空间划分
求精
抽象
Ltl模型检测
应用模型
状态空间爆炸
方法
空间复杂度
逐步求精
数值实验
检测
工业系统
障碍
验证
效率
消减
内存
|
| 部门归属 | 中国科学院软件所,计算机科学国家重点实验室,北京,100080;School of Computing and Mathematics University of Western Sydney, Sydney 2747,Australia;中国科学院软件所,计算机科学国家重点实验室,北京,100080
|
| 语种 | 中文
|
| 内容类型 | 期刊论文
|
| URI标识 | http://ir.iscas.ac.cn/handle/311060/11298
|
| 专题 | 基础软件与系统重点实验室
|
推荐引用方式
GB/T 7714 |
蒲飞,张文辉. 结合搜索空间划分和抽象进行LTL模型检测[J]. 中国科学E辑,2007,37(12):1504-1520.
|
| APA |
蒲飞,&张文辉.(2007).结合搜索空间划分和抽象进行LTL模型检测.中国科学E辑,37(12),1504-1520.
|
| MLA |
蒲飞,et al."结合搜索空间划分和抽象进行LTL模型检测".中国科学E辑 37.12(2007):1504-1520.
|
除非特别说明，本系统中所有内容都受版权保护，并保留所有权利。
修改评论