Title: On combining the ready sets with the covering steps methods

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.

DOI: 10.1504/IJCCBS.2014.059591

International Journal of Critical Computer-Based Systems, 2014 Vol.5 No.1/2, pp.55 - 77

Published online: 21 Oct 2014 *

Full-text access for editors Full-text access for subscribers Purchase this article Comment on this article