Using inclusion abstraction to construct Atomic State Class Graphs for Time Petri Nets. (6th July 2006)

• Record Type: Journal Article
• Authors: Boucheneb, Hanifa; Hadjidj, Rachid
• Is Part Of: International journal of embedded systems. Volume 2:Number 1/2(2006)
• Page Start: 128
• Page End: 139
• Publication Date: 2006-07-06
• Subjects: time petri nets -- TPN -- state class spaces -- strong state class graphs -- SSCG -- atomic state class graphs -- ASCG -- CTL* properties -- model checking -- inclusion abstraction; Embedded computer systems -- Periodicals; 004.16
• Languages: English
• ISSNs: 1741-1068

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).