Lazy Slicing for State-Space Exploration

• Published in: Journal of computer science and technology 2012-07, Vol.27 (4), p.872-890
• Main Author: 黄少滨 黄宏涛 陈志远 吕天阳 张涛
• Format: Article
• Language: English
• Subjects: Algorithms; Analysis; Artificial Intelligence; Checkers; Computer programming; Computer Science; Computer simulation; Construction costs; Cost control; Cost engineering; Data Structures and Information Theory; Exploration; Information Systems Applications (incl.Internet); Mathematical models; Regular Paper; Slicing; Software; Software Engineering; Space exploration; Studies; Theory of Computation; Variables; 切片; 太空探索; 抽象; 模型检查; 状态空间; 空间处理; 财产安全; 路径
• ISSN: 1000-9000; 1860-4749
• DOI: 10.1007/s11390-012-1271-7

CEGAR （Counterexample-guided abstraction refinement）-based slicing is one of the most important techniques in reducing the state space in model checking. However, CEGAR-based slicing repeatedly explores the state space handled previously in case a spurious counterexample is found. Inspired by lazy abstraction, we introduce the concept of lazy slicing which eliminates this repeated computation. Lazy slicing is done on-the-fly, and only up to the precision necessary to rule out spurious counterexamples. It identifies a spurious counterexample by concretizing a path fragment other than the full path, which reduces the cost of spurious counterexample decision significantly. Besides, we present an improved over-approximate slicing method to build a more precise slice model. We also provide the proof of the correctness and the termination of lazy slicing, and implement a prototype model checker to verify safety property. Experimental results show that lazy slicing scales to larger systems than CEGAR-based slicing methods.