Tctl_h^Δ model checking of time petri nets

Concurrent systems are becoming tremendous in different fields such as network applications, communication protocols and client server applications. However, they are rather difficult to develop and especially, due to concurrency, these systems are faced to specific errors like deadlocks and livelocks. In this context, model checking is a promising formal method which permits systems analysis at early stage, thus ensuring prevention from errors occurring. In previous work [16], we proposed an extension of timed temporal logic TCTL with more powerful modalities aiming to specify properties with clocks quantifiers as well as features for transient states. We formally defined the syntax and the semantics of the proposed quantitative logic called TCTL_h^Δ.Aswellas in [15], we used timed automata and region graph to discuss the applicability of the proposal to model checking by studying its decidability and complexity. In this paper, we define a timed temporal logic TPN-TCTLf_h^Δ for time Petri nets, for which model-checking is PSPACE-complete. In fact, Petri nets in general have gained a special interest due to their expressiveness power especially while dealing with concurrency. After detailing the proposed model checking method, we show its development and integration into the tool Romeo. Finally, we prove the efficiency of the method via case studies and simulation results.