We present a method for computing abstractions of infinite state systems compositionally and automatically. Given a concrete system S = S₁ || ... || S_n of programs and given an abstraction function a, using our method one can compute an abstract system S^a = S^a₁ || ... || S^a_n such that S simulates S^a. A distinguishing feature of our method is that it does not produce a single abstract state graph but rather preserves the structure of the concrete system. Tills feature is a prerequisite to ben efit from the techniques developed in the context of model-checking for mitigating the state explosion. Moreover, our method has the advantage that the process of constructing the abstract system does not depend on whether the computation model is synchronous or asynchronous.

• cav98.ps