A method for the verification of a distributed and synchronized algorithm

In the model-checking context, the method used to detect stable properties is to construct the synchronized product of the input automata. The problem with such a method is the well-known state space explosion. We present a new algorithm that allows us to restrict this explosion, by constructing only the states necessary to check the stable properties. The basic idea is to forget the states that are not relevant to the verification. This is done by aggregating the concurrent transitions.