节点文献

结合搜索空间划分和抽象进行LTL模型检测

  • 推荐 CAJ下载
  • PDF下载
  • 不支持迅雷等下载工具，请取消加速工具后下载。

【作者】 蒲飞； 张文辉；

【机构】 中国科学院软件所计算机科学国家重点实验室； 中国科学院软件所计算机科学国家重点实验室 北京100080 School of Computing and Mathematics； University of Western Sydney； Sydney 2747 Australia； 北京100080；

【摘要】 在应用模型检测于工业系统时,状态空间爆炸仍然是一个主要的障碍.基于抽象的方法在克服状态空间爆炸方面取得了很大的成功.提出一种结合搜索空间划分和抽象的方法来降低模型检测的空间复杂度.划分依赖于每个所分划的搜索空间的表达.特别地,划分可以逐步求精以获得更好的空间消减.从数值实验看,这种搜索空间划分和抽象的结合在基于内存的需求上能提高验证的效率,同时能得到比单独使用其中一种方法更好的效果.

【关键词】 搜索空间划分； 求精； 抽象； LTL模型检测；
【基金】 国家自然科学基金(批准号:60573012,60421001);国家重点基础研究发展规划(批准号:2002cb312200)资助项目
  • 【文献出处】 中国科学(E辑:信息科学) ,Science in China(Series E:Information Sciences) , 编辑部邮箱 ,2007年12期
  • 【分类号】TP311.52
  • 【被引频次】10
  • 【下载频次】223
打印本页
节点文献中：