Collapsing Reachability Graphs

Reachability graphs are commonly used for the description of protocol specifications as dynamic systems. However, the size of such graphs may be extremely large, making protocols unmanageable even if automated tools are used in the analysis of such protocol specifications. For this reason, any technique for reducing the size of these graphs, while preserving the basic functional properties, is most welcome. In this paper, we explore the complexity of collapsing the reachability graph into a simpler graph that can still be used to answer questions about paths in the graph. Our collapsing is such that no "new paths" are created in the graph. It seems intuitive that such a restriction should be enforced, since the reachability aspect of protocols is closely related to paths in reachability graphs. We show that the version of such a problem belongs to the family of NP-Complete problems, and that even a good approximation algorithm is unlikely to exist. We also prove that the problem is easily resolved when the reachability graph satisfies certain sufficient conditions.