Aggregation of states in colored stochastic Petri nets: application to a multiprocessor architecture

A lumping method that is based on a particular class of colored Petri nets is presented. The originality of the method is that the states are aggregated a priori, thus avoiding the construction of the whole reachability graph. The authors construct only a graph of symbolic markings whose states are classes of markings and from which the solution can be directly computed. They show on an example that the method can be usefully applied to the performance evaluation of symmetric systems