Model checking of time Petri nets

The intention of the paper is to develop a model checking algorithm for real time systems represented by time Petri nets and a real time extension of the branching time temporal logic CTL, called TCTL. Since time Petri nets model real time systems over dense time domain, the number of states of any net is infinite. Using a notion of region, we construct a finite representation of the behaviour of a time Petri net - the region graph - to which model-checking algorithm can be applied. Some results about the complexity of the model checker proposed are given.