کد مقاله | کد نشریه | سال انتشار | مقاله انگلیسی | نسخه تمام متن |
---|---|---|---|---|
439378 | 690540 | 2006 | 20 صفحه PDF | دانلود رایگان |

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.
Journal: Theoretical Computer Science - Volume 353, Issues 1–3, 14 March 2006, Pages 208-227