Title: Using inclusion abstraction to construct Atomic State Class Graphs for Time Petri Nets

Authors: Hanifa Boucheneb, Rachid Hadjidj

Addresses: Department of Computer Engineering, Ecole Polytechnique de Montreal, P.O. Box 6079, Station Centre-ville, Montreal, Quebec, Canada. ' Department of Computer Engineering, Ecole Polytechnique de Montreal, P.O. Box 6079, Station Centre-ville, Montreal, Quebec, Canada

Abstract: We show in this paper how to contract the TPN state space into a graph that captures all its CTL* properties. This graph, called Atomic State Class Graph (ASCG), is finite if and only if, the model is bounded. To achieve this objective, we use a refinement technique similar to what is proposed in Berthomieu and Vernadat (2003) and Yoneda and Ryuba (1998). In such a technique, an intermediate contraction of the TPN state space is first built then refined until CTL* properties are restored. Compared with the approaches in Berthomieu and Vernadat (2003) and Yoneda and Ryuba (1998), we use inclusion abstraction during all phases of the construction process while reducing the complexity of computations. Our approach allows us to construct smaller ASCGs in shorter times (more than five times faster in certain cases).

Keywords: time petri nets; TPN; state class spaces; strong state class graphs; SSCG; atomic state class graphs; ASCG; CTL* properties; model checking; inclusion abstraction.

DOI: 10.1504/IJES.2006.010171

International Journal of Embedded Systems, 2006 Vol.2 No.1/2, pp.128 - 139

Published online: 05 Jul 2006 *

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