Symmetry reduced state classes for time petri nets

Abstract

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.

Publication
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