Colored GSPN models and automatic symmetry detection

Colored Petri nets (CPN) are useful for the development of very compact and easy to understand models of systems with interacting concurrent components. A CPN model can be used for a qualitative analysis of the modeled system; when timing is also added, a quantitative analysis can be done. Unfortunately, the analysis can be prevented by excessive size of the reachability graph (RG) of the net, which can grow exponentially as a function of the number of places and the cardinality of color domains. A method that automatically exploits the symmetries intrinsic in the model reducing the RG size is presented: it can be applied to a subclass of CPNs called regular nets (RN). Some nontrivial examples are presented to demonstrate that the automatically achieved reductions are comparable to those devised for these systems by thoroughly studying their behavior