Using multi decision diagram in model checking

Abstract

Model checking[1] is an automatic verification technique for finite concurrent systems. In this method, the assertion is verified by exhaustively searching over the state space. However, the number of states of the system will grow exponentially with the number of processes. It limits model checker to handle with complex systems. In explicit model checking[1], system states are explored one-by-one and stored in memory explicitly, so the verified system is restricted by the memory resource. Most of the memory is consumed by the hash table which contains the visited states and the queue of states whose successors are already generated. In this paper, we will present a new way of storing the visited states by using a tree. We show that our approach is memory efficient. Organization of the report: Section 1 is the introduction, and section 2 introduces PAT model checker. Section 3 describes how to implement the tree storing the visited states. Section 4 presents the heuristic to improve the performance for the tree. Section 5 is the experiment result. Lastly section 6 is the conclusion and future work. © 2010 IEEE.