| 结合搜索空间划分和抽象进行LTL模型检测 |
| |
| 作者姓名： | 蒲飞 张文辉 |
| |
| 作者单位： | 1. 中国科学院软件所,计算机科学国家重点实验室,北京,100080;School of Computing and Mathematics University of Western Sydney, Sydney 2747,Australia
2. 中国科学院软件所,计算机科学国家重点实验室,北京,100080 |
| |
| 基金项目： | 国家自然科学基金;国家重点基础研究发展规划(973计划) |
| |
| 摘 要： | ![]()
在应用模型检测于工业系统时,状态空间爆炸仍然是一个主要的障碍.基于抽象的方法在克服状态空间爆炸方面取得了很大的成功.提出一种结合搜索空间划分和抽象的方法来降低模型检测的空间复杂度.划分依赖于每个所分划的搜索空间的表达.特别地,划分可以逐步求精以获得更好的空间消减.从数值实验看,这种搜索空间划分和抽象的结合在基于内存的需求上能提高验证的效率,同时能得到比单独使用其中一种方法更好的效果.
|
| 关 键 词： | 搜索空间划分 求精 抽象 LTL模型检测 |
| 收稿时间： | 2007-04-30 |
| 修稿时间： | 2007-07-20 |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ |
|
