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

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 similarly to what is proposed in Berthomieu and Vernadat (2003) and Yoneda and Ryuba (1998). In such technique, an intermediate contraction of the TPN state space is first built then refined until CTL* properties are restored. Comparing 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 to construct smaller ASCGs in shorter times (more than five times faster in certain cases).