model checking for time Petri nets

This paper aims at applying the CTL*1, model checking method to the time Petri net (TPN) model. We show here how to contract its generally infinite 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.2 Our approach is based on a partition refinement technique, similarly to what is proposed in [Berthomieu, Vernadat, State class constructions for branching analysis of time Petri nets, Lecture Notes in Computer Science, vol. 2619, 2003; Yoneda, Ryuba, CTL model checking of time Petri nets using geometric regions, IEICE Trans. Inf. Syst. E99-D(3) (1998)]. In such a technique, an intermediate abstraction (contraction) of the TPN state space is first built, then refined until CTL* properties are restored. Our approach improves the construction of the ASCG in two ways. The first way deals with speeding up the refinement process by using a much more compact intermediate contraction of the TPN state space than those used in [Berthomieu, Vernadat, State class constructions for branching analysis of time Petri nets, Lecture Notes in Computer Science, vol. 2619, 2003; Yoneda, Ryuba, CTL model checking of time Petri nets using geometric regions, IEICE Trans. Inf. Syst. E99-D(3) (1998)]. The second way deals with computing each ASCG node in O(n2) instead of O(n3), n being the number of transitions enabled at the node. Experimental results have shown that our improvements have a good impact on performances.