Symbolic path-based protocol verification

The principal problem in protocol verification is state explosion problem. In our work (W.C. Liu, C.G. Chung, Path-based Protocol Verification Approac h, Technical Report, Department of Computer Science and Information Enginee ring, National Chiao-Tung University, Hsin-Chu, Taiwan, ROC, 1998), we have proposed a "divide and conquer" approach to alleviate this problem, the pa th-based approach. This approach-separates the protocol into a set of concu rrent paths, each of which can be generated and verified independently of t he others. However, reachability analysis is used to identify the concurren t paths from the Cartesian product of unit paths, and it is time-consuming. Therefore,:in this paper, we propose a simple and efficient checking algor ithm-to identify the concurrent paths from the Cartesian product, using onl y Boolean and simple arithmetic operations. (C) 2000 Elsevier Science B.V; All rights reserved.