Symmetry reduction for time Petri net state classes

We propose a method to exploit the symmetries of a real-time system represented by a Time Petri net for its verification by model-checking. The method handles both markings and timing constraints; it can be used in conjunction with the widely used state classes abstraction, a construction providing a finite representation of the behavior of a Time Petri net preserving its markings and traces. The approach has been implemented and experiments are reported.