Symmetry reduced state classes for Time Petri nets

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

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

We propose a method to exploit the symmetries of a realtime system represented by a Time Petri net for its verification by model-checking. Instead of computing states, symmetry reduction methods compute equivalence classes of states for the symmetry relation. Methods for alleviating state explosion are even more important for realtime systems since time constraints makes alternatives to enumerative approaches more difficult to apply. Dense-time timed systems generally have infinite state spaces; obtaining finite representations for model checking involves some abstractions. Typically, the state information is represented by composite abstract states capturing a discrete information together with a timing information. The paper introduces a symmetry reduction method for Time Petri nets applicable to the well known state classes abstraction of their state space. The approach has been implemented and computing experiments are reported.

Mots clés: Model-Checking; Time Petri Nets

Domaines: Systèmes embarqués; Logique en informatique [cs.LO]

Pierre-Alain Bourdil, Bernard Berthomieu, Silvano Dal Zilio, François Vernadat. Symmetry reduced state classes for Time Petri nets. 30th Annual ACM Symposium on Applied Computing, Apr 2015, Salamanca, Spain. pp.1751-1758, ⟨10.1145/2695664.2695803⟩. ⟨hal-01275316⟩