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

In order to establish time properties of real time systems, we consider its time Petri net (TPN) model. First, we will prove that properties like minimal (or maximal) firing date, minimal (or maximal) time interval between firing of two transitions can be established with a discrete analysis of time Petri net. Then we propose to express all the discrete execution sequence of the TPN by an automaton considering discrete elapsing of time as the occurrence of a dedicated event. The advantage is that this automaton can be efficiently analysed by Binary Decision Diagrams. We have implemented every step of this approach.