[BBc14] Delay-Dependent Partial Order Reduction Technique for Time Petri NetsConférence Internationale avec comité de lecture : 12th International Conference, FORMATS 2014 - Lecture Notes in Computer Science , September 2014, Vol. 8711, pp. 53-68, Series Lecture Notes in Computer Science, (DOI: 10.1007/978-3-319-10512-3_5)
Mots clés: Partial order reduction techniques ; Time Petri Nets
Résumé: Partial order reduction techniques aim at coping with the state explosion problem by reducing, while preserving the properties of interest, the number of transitions to be fired from each state of the model. For (time) Petri nets, the selection of these transitions is, generally, based on the structure of the (underlying) Petri net and its current marking. This paper proposes a partial order reduction technique for time Petri nets (TPN in short), where the selection procedure takes into account the structure, including the firing intervals, and the current state (i.e., the current marking and the firing delays of the enabled transitions). We show that our technique preserves non-equivalent firing sequences of the TPN. Therefore, its extension to deal with LTL − X properties is straightforward, using the well established methods based on the stuttering equivalent sequences.