A new decomposition method to relieve the state space explosion problem

Reachability analysis has proved to be one of most effective methods for protocol verification, but it is well known that it suffers from the state space explosion problem. In this paper, we present a new approach to generating state space in order to help relieve the state space explosion problem. In this approach, state space is generated and verified in stages. That is, only one subspace is involved in each stage of verification; upon completion, the memory occupied by a particular subspace can be released and subsequently used by the next subspace. The amount of memory needed for the verification of the whole protocol can be dramatically reduced, and thus the explosion problem relieved