Title: 结合搜索空间划分和抽象进行LTL模型检测
Author: 蒲飞
; 张文辉
Keyword: 搜索空间划分
; 求精
; 抽象
; LTL模型检测
; 应用模型
; 状态空间爆炸
; 方法
; 空间复杂度
; 逐步求精
; 数值实验
; 检测
; 工业系统
; 障碍
; 验证
; 效率
; 消减
; 内存
Source: 中国科学E辑
Issued Date: 2007
Volume: 37, Issue: 12, Pages: 1504-1520 Department: 中国科学院软件所,计算机科学国家重点实验室,北京,100080;School of Computing and Mathematics University of Western Sydney, Sydney 2747,Australia;中国科学院软件所,计算机科学国家重点实验室,北京,100080
Abstract: 在应用模型检测于工业系统时, 状态空间爆炸仍然是一个主要的障碍. 基于抽象的方法在克服状态空间爆炸方面取得了很大的成功. 提出一种结合搜索空间划分和抽象的方法来降低模型检测的空间复杂度. 划分依赖于每个所分划的搜索空间的表达. 特别地, 划分可以逐步求精以获得更好的空间消减. 从数值实验看, 这种搜索空间划分和抽象的结合在基于内存的需求上能提高验证的效率, 同时能得到比单独使用其中一种方法更好的效果.
Language: 中文
Content Type: 期刊论文
URI: http://ir.iscas.ac.cn/handle/311060/11298
Appears in Collections: 计算机科学国家重点实验室 _期刊论文
File Name/ File Size
Content Type
Version
Access
License
结合搜索空间划分和抽象进行LTL模型检测.pdf (823KB) -- -- 限制开放 -- 联系获取全文
Recommended Citation:
蒲飞,张文辉. 结合搜索空间划分和抽象进行LTL模型检测[J]. 中国科学E辑,2007-01-01,37(12):1504-1520.