Temporal reduction in time Petri net

Temporal analysis of large real-time systems expressed in terms of formal timed models such as time Petri net (TPN) faces to the problem of combinatory explosion. In practice, a complex system model is made of components, of which TPN models are called modules. Since timed properties that must be checked on a real-time system do not generally imply the whole discrete events of the system, we propose a solution based on the hiding of internal events of the modules, followed by a reduction of these modules preserving the property to check. The purpose is to lighten the cost of a verification on a global system thanks to abstract view of some modules. Under some hypotheses, this paper shows that reduction of a module can be very efficient by limiting ourself to necessary connections with the environment of the module, while preserving temporal specifications. This methodology combines theories on unfolding, verification and reduction.