Behaviour analysis of parametric time Petri nets

We introduce a new notion of parametric time Petri nets, an extension of time Petri nets whose transitions are labelled with parametric time restrictions. Further, a time behaviour analysis algorithm for the real time branching time temporal logic TCTL and a one-safe parametric time Petri net is proposed. The result of the algorithm is a set of conditions on parameter variables which is sufficient for the property expressed as a TCTL-formula being satisfied for a given parametric time Petri net. Some remarks about complexity of the algorithm are also given.