Article Preview
Top1. Introduction
Nowadays, the emergent systems are becoming more and more complex due to not only the distributed nature of the involved elements but also the real time constraints. For the efficient specification and verification of these systems, Time Petri nets (TPN) (Merlin (1974) refer to one of the most common formal models used for their expressive power, graphical notation and availability of various tools based on them. Time Petri nets extend Petri nets with the fact that the transition firing is possible after a certain elapse of time from the enabled transition. They differ from Timed Petri nets where duration is assigned to each transition.
Among many existing representations of time information on Petri nets, the authors focus on Petri nets augmented by associating to each transition a static firing interval. This model is the same referred to as Time Petri net (TPN) firstly proposed in (Merlin (1974) and widely studied in the literature (Khansa et al. (1996), Berthomieu & Diaz (1991), de Frutos-Escrig et al. (2000))
Associated with model checking techniques, TPN were especially widely used for the formal verification purpose. Among the recent works, in (Jbeli et al. (2016A)) the authors addressed the issue by analyzing concurrent and distributed systems with using an extension of the TCTL temporal logic. This work is interesting since it permits to verify properties and it explicits durations as well as activation delays. For this, they combined the two fragments 
.and 
.to propose
. The logic 
. studied by (Laroussinie (2005), extends TCTL with a capability to reset clocks, while the logic fragment 
. introduced by Bel Mokadem (Mokadem et al. (2006)), permits modalities of kind 
.expecting 
.to hold for k units of time. The authors studied in (Jbeli et al. (2017)) the decidability and complexity of 
.and prove its PSPACE-completeness. Then, in (Jbeli et al. (2016B)), 
.is proposed to deal with GMECs (the specification of Petri net markings) instead of atomic properties, leading to an extension of TCTL on TPN called
.
Despite its importance, the theoretical side of the model checking based verification suffers in general from limitations in practice due to the exponential number of the reachable states, which is the base for applying this technique. For this, “on the fly” techniques are used in (Jbeli et al. (2018)) to present an efficient technique for the 
.model checking on bounded 
.nd implement it in Romeo model checker (Gardey et al. (2005)). The challenge in this paper is to propose an improved version of the 
.model checking by searching a reduced number of reachable states while executing the on the fly model checking algorithm.