Skip to main content

Symmetry reduction for time Petri net state classes

Verification Time Petri Nets Tina
Table of Contents

Pierre-Alain Bourdil, Bernard Berthomieu, Silvano Dal Zilio, François Vernadat
Science of Computer Programming 132(2):209—225, aug 2016.

journal

 PDF  DOI〈10.1016/j.scico.2016.08.008〉  HAL-01561994

Abstract
#

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.

Citation
#


@Article{DalzilioS:scp2016symmetries,
   author  = {Bourdil, Pierre-Alain and Berthomieu, Bernard and {Dal Zilio}, Silvano and Vernadat, François},
   title   = {{Symmetry reduction for time Petri net state classes}},
   journal = {Science of Computer Programming},
   number  = {2},
   volume  = {132},
   doi = {10.1016/j.scico.2016.08.008},
   pages   = {209--225},
   month   = aug, 
   year    = 2016
}