Compositional reachability analysis using process algebra

Abstract

State explosion is the primary obstacle to practical application of reachability analysis techniques for concurrent systems. State explosion can be substantially controlled by using process algebra to achieve compositional (divide-and-conquer) analysis. A prototype tool incorporating process algebra is described. The promise and problems of the approach are illustrated by applying the tool to an example that incorporates the alternating bit protocol as a module.