Authors: Hanifa Boucheneb; Kamel Barkaoui
Addresses: 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
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.
International Journal of Critical Computer-Based Systems, 2014 Vol.5 No.1/2, pp.55 - 77
Published online: 02 Mar 2014 *Full-text access for editors Access for subscribers Purchase this article Comment on this article