Symmetry reduced state classes for time petri nets


We propose a method to exploit the symmetries of a realtime 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. The approach has been implemented and experiments are reported.

In SAC 201530th Annual ACM Symposium on Applied Computing
  • An extended version appears in Science of Computer Programming 132(2):209-225, Aug 2016. URL