In: etfa2001, 8th IEEE International Conference on Emerging Technologies and Factory Automation, pages Volume 2, 197-204. October 2001. IEEE Catalog number : 01TH8597.
Abstract: In order to check 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.
Keywords: Time Petri Nets, discrete time, Model-checking.