Symmetry reduced state classes for Time Petri nets

International audienceWe propose a method to exploit the symmetries of a realtime systemrepresented by a Time Petri net for its verification bymodel-checking. Instead of computing states, symmetry reductionmethods compute equivalence classes of states for the symmetryrelation. Methods for alleviating state explosion are even moreimportant for realtime systems since time constraints makesalternatives to enumerative approaches more difficult to apply.Dense-time timed systems generally have infinite state spaces;obtaining finite representations for model checking involves someabstractions. Typically, the state information is represented bycomposite abstract states capturing a discrete information togetherwith a timing information. The paper introduces a symmetry reductionmethod for Time Petri nets applicable to the well known state classesabstraction of their state space. The approach has been implementedand computing experiments are reported