Time Arc Petri Nets and Their Analysis

We propose to extend time arc Petri nets by associating with each transition a strong or a weak firing semantics. The proposed model includes the semantics of existing time Petri nets where time intervals are associated with places, transitions and arcs in their weak and strong semantics. We show afterwards that state space abstraction techniques for constructing zone graphs can be adapted to the proposed model. For the theory of time Petri nets this result gives the decidability of k-boundedness, marking reachability and language emptiness problems for the proposed model and all its sub-classes.