An improved decomposition approach for reachability analysis

Reachability analysis has proved to be one of the most effective methods for protocol verification, because it can verify a large set of safety properties such as boundedness, livelock freeness, deadlock freeness, etc. It is well known that the state space explosion is the most severe limitation to the applicability of this method. Various approaches have been proposed to deal with the problem. In a previous paper, (see Proceedings 5th Internat. Conf. Computing and Inform., Sudbury, Canada, IEEE, 1993) the authors proposed a new approach to generating state space in order to help relieve the state space explosion problem and the verification algorithms involved in this method. In this paper, the verification algorithm, one of the important components of the method, is significantly improved