Abstract (EN)

An extension of regular nets, a class of colored nets, to a stochastic model is proposed. We show that the symmetries in this class of nets make it possible to develop a performance evaluation by constructing only a graph of symbolic markings, which vertices are classes of states, instead of the whole reachability graph. Using algebraic techniques, we prove that all the states in a class have the same probability, and that the coefficients of the linear system describing the lumped Markov process can be calculated directly from the graph of symbolic markings.