| Combining search space partition and abstraction for LTL model checking |
| |
| 作者单位： | PU Fei（State Key Laboratory of Computer Science,Institute of Software, Chinese Academy of Sciences, Beijing 100080,China;School of Computing and Mathematics,University of Western Sydney, Australia） ;
ZHANG WenHui（State Key Laboratory of Computer Science,Institute of Software, Chinese Academy of Sciences, Beijing 100080,China） ; |
| |
| 基金项目： | Supported by the National Natural Science Foundation of China (Grant Nos. 60573012 and 60421001)，the National Grand FundamentalResearch 973 Program of China (Grant No. 2002cb312200) |
| |
| 摘 要： | The state space explosion problem is still the key obstacle for applying model checking to systems of industrial size. Abstraction-based methods have been particularly successful in this regard. This paper presents an approach based on refinement of search space partition and abstraction which combines these two techniques for reducing the complexity of model checking. The refinement depends on the representation of each portion of search space. Especially, search space can be refined stepwise to get a better reduction. As reported in the case study, the integration of search space partition and abstraction improves the efficiency of verification with respect to the requirement of memory and obtains significant advantage over the use of each of them in isolation.
|
| 收稿时间： | 12 December 2005 |
| 修稿时间： | 26 July 2007 |
Combining search space partition and abstraction for LTL model checking |
| |
| Authors: | Pu Fei Zhang WenHui |
| |
| Affiliation: | (1) State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Beijing, 100080, China;(2) School of Computing and Mathematics, University of Western Sydney, Australia |
| |
| Abstract: | The state space explosion problem is still the key obstacle for applying model checking to systems of industrial size. Abstraction-based methods have been particularly successful in this regard. This paper presents an approach based on refinement of search space partition and abstraction which combines these two techniques for reducing the complexity of model checking. The refinement depends on the representation of each portion of search space. Especially, search space can be refined stepwise to get a better reduction. As reported in the case study, the integration of search space partition and abstraction improves the efficiency of verification with respect to the requirement of memory and obtains significant advantage over the use of each of them in isolation. |
| |
| Keywords: | search space partition refinement abstraction LTL model checking |
| 本文献已被 SpringerLink 等数据库收录！ |
