A Novel Learning Framework for State Space Exploration Based on Search State Extensibility Relation

Model Checking is an effective method for design verification, useful for proving temporal properties of the underlying system. In model checking, computing the pre-image (or image) space of a given temporal property plays a critical role. In this paper, we propose a novel learning framework for efficient state space exploration based on search state extensibility relation. This allows for the identification and pruning of several non-trivial redundant search spaces, thereby reducing the computational cost. We also propose a probability-based heuristic to guide our learning method. Experimental evidence is given to show the practicality of the proposed method.