Discrete time approach of time Petri nets for real-time systems analysis

In order to establish the temporal properties of real-time systems, we consider the timed Petri net (TPN) model. First, we prove that properties like the minimal (or maximal) firing time and the minimal (or maximal) time interval between the firing of two transitions can be established with a discrete analysis of a TPN. Then we propose to express the entire discrete execution sequence of the TPN by an automaton which considers the discrete passing of time as the occurrence of a dedicated event. The advantage is that this automaton can be efficiently analysed by using binary decision diagrams (BDDs). We have implemented every step of this approach.