Title: On combining the ready sets with the covering steps methods
Author: Hanifa Boucheneb; Kamel Barkaoui
Laboratoire VeriForm, Department of Computer Engineering, École Polytechnique de Montréal, P.O. Box 6079, Station Centre-ville, Montréal, Québec, H3C 3A7, Canada
Laboratoire CEDRIC, Conservatoire National des Arts et Métiers, 292 rue Saint Martin, Paris Cedex 03, France
Journal: Int. J. of Critical Computer-Based Systems, 2014 Vol.5, No.1/2, pp.55 - 77
Abstract: We consider here time Petri nets and the covering steps graph technique proposed by Vernadat et al. for untimed Petri nets. In this technique, some transitions are put together to be fired in a single transition step. This paper investigates how this technique can be extended to be applied to time Petri nets. It establishes some sufficient conditions useful to construct covering steps graphs preserving LTL−X. Finally, it investigates how the covering steps graph can be combined together with a partial order technique, in the context of time Petri nets, to attenuate further the state explosion problem, while preserving LTL−X.
Keywords: time Petri nets; TPN; state class graph method; covering steps graph; partial order techniques.
Available online 02 Mar 2014