Towards Scalable Compositional Analysis

Abstract

Due to the state explosion problem, analysis of large concurrent programs will undoubtedly require compositional techniques. Existing compositional techniques are based on the idea of replacing complex subsystems with simpler processes with the same interfaces to their environments, and using the simpler processes to analyze the full system. Most algorithms for proving equivalence between two processes, however, require enumerating the states of both processes. When part of a concurrent system consists of many highly coupled processes, it may not be possible to decompose the system into components that are both small enough to enumerate and have simple interfaces with their environments. In such cases, analysis of the systems by standard methods will be infeasible. In this paper, we describe a technique for proving trace equivalence of deterministic and divergence-free systems without enumerating their states. (For deterministic systems, essentially all the standard notions of process...