Towards TCTLhΔ model checking of Time Petri Nets

At present, the most common method for verifying that a system met its specifications or to detect unexpected behavior and issues is to perform simulations on the model. This approach is limited by the fact that it is of course impossible to be exhaustive and fully test the system. This is why the need to resort to formal methods, and more particularly to model-checking, was felt. In this paper, we are interested by modeling the behavior of real time systems using time Petri nets. Our main objective is to present new model checking algorithms for our new logic called TCTLh Delta new which is the combination of the two extensions of the TCTL logic TCTLh and TCTLh Delta. These algorithms are based on the concept of on the fly verification and are implemented into the model checker Romeo.