Symmetry reduction for time Petri net state classes

Pierre-Alain Bourdil (1) , Bernard Berthomieu (1) , Silvano Dal Zilio (1) , François Vernadat (1, 2)

1 LAAS-VERTICS - Équipe Verification de Systèmes Temporisés Critiques
2 INSA Toulouse - Institut National des Sciences Appliquées - Toulouse

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.

Mots clés: Time Petri Nets; State Classes; Symmetry Reduction

Domaines: Informatique [cs]; Génie logiciel [cs.SE]

Pierre-Alain Bourdil, Bernard Berthomieu, Silvano Dal Zilio, François Vernadat. Symmetry reduction for time Petri net state classes. Science of Computer Programming, 2016, Science of Computer Programming, 132 (Part 2), pp.209 - 225. ⟨10.1016/j.scico.2016.08.008⟩. ⟨hal-01561994⟩