In this paper we present a method for the compositional construction of the minimal transition system that represents the semantics of a given distributed system. Our aim is to control the state explosion caused by the interleavings of actions of communicating parallel components by reduction steps that exploit global communication constraints given in terms of interface specifications. The effect of the method, which is developed for bisimulation semantics here, depends on the structure of the distributed system under consideration, and the accuracy of the interface specifications. However, its correctness does not: every "successful" construction is guaranteed to yield the desired minimal transition sytem, independent of the correctness of the interface specifications provided by the program designer.
Ulrike Peiker, Martin Griebl