On reachability and reverse reachability analysis of communicating finite state machines

Reachability analysis and reverse reachability analysis are two important verification techniques for communicating finite state machines (CFSMs). The issue of the relative efficiency of reachability analysis and reverse reachability analysis is still unsettled. We first propose a new theory of reachability and reverse reachability analysis. Based on the new theory we discuss and analyze the suitability of these two reachability analysis methods. We then present a reachability evaluator, which, given any network of CFSMs, will try to estimate the sizes of the reachable and reverse reachable state spaces by taking snapshots of the reachability and reverse reachability spaces. The core of the evaluator is the notion of random state generation with seed states, which extends the idea of random state exploration proposed by West (1986). Results from example applications have shown that the evaluator provides guidance in choosing the better of the two methods.