Using Multi Decision Diagram in Model Checking
Model checking 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, 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.