CTL model checking for time Petri nets

• Published in: Theoretical computer science 2006-03, Vol.353 (1), p.208-227
• Main Authors: Boucheneb, Hanifa, Hadjidj, Rachid
• Format: Article
• Language: English
• Subjects: [formula omitted] properties; Algorithmics. Computability. Computer arithmetics; Applied sciences; Atomic state class graph; Automata. Abstract machines. Turing machines; Computer science; control theory; systems; Exact sciences and technology; Logic and foundations; Mathematical logic, foundations, set theory; Mathematics; Model checking; Model theory; Sciences and techniques of general use; State class spaces; Strong state class graph; Theoretical computing; Time Petri nets
• ISSN: 0304-3975; 1879-2294
• DOI: 10.1016/j.tcs.2005.11.002

This paper aims at applying the CTL * 1 1 Computation Tree Logic. 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 2 The number of its reachable markings is finite. 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 ( n 2 ) instead of O ( n 3 ) , n being the number of transitions enabled at the node. Experimental results have shown that our improvements have a good impact on performances.