Symmetries in stochastic Petric nets - Construction of the symbolic graph

The main purpose of this paper is to give a method for construction of the reduced reachability graph for Stochastic Petri Nets (SPN), the symbolic gr aph. This construction is achieved by exploiting the structural symetries i n the net using the theory of bisimulation of places for detecting isomorph ic parts in the net. The symbolic graph, being isomorphic to an agregated M arkov chain, may be used to prove qualitative properties as liveness, bound ness,... Moreover, this reduced graph make more easy the computation of the performance measures of interest as the mean number of tokens in a place, the mean number of firing transition... We have so developped a tool, SSPN (Stochastic Symetric Petri nets), far generating the symbolic graph and ded ucing qualitatives and quantitatives properties.