Finding reachable states of finite-state concurrent systems
Abstract We present detailed algorithms for finding, for a given finitestate concurrent software system, all states reachable from a given set of possible initial states. Our systems consist of processes that send and receive messages through links of bounded capacity. Input to the algorithm is a software system, described in a modeling notation that resembles a programming language. Of particular interest are the techniques for modeling the effects of concurrency and nondeterminism, for detecting infinite loops, and for selecting a set of particularly significant states to report to the user. We discuss performance of the algorithms and provide data from implementations.