Reusing Symbolic Observation Graph for Efficient Model Checking

Model checking is a powerful and widespread technique for the verification of finite state concurrent systems. In practice, the most challenging obstacle of this technique is the state space explosion. There is much research on state space reduction techniques for model checker. Notably, Symbolic Observation Graph (SOG) is a technique which produces an abstracted graph to reduce the state space to be checked. However, the drawback of this approach is that it is extremely time consuming for the construction of SOG. Therefore, in this paper, we propose a novel technique to optimize the construction of SOG by reusing the previously constructed SOGs when verifying other properties. Experimental results show that our technique is more efficient than both the explicit model checking and the original SOG technique.