Towards Efficient Partial Order Techniques for Time Petri Nets

Time Petri nets (TPN for short) are established as a powerful formalism for modeling and verifying systems with explicit soft and hard time constraints. However, their verification techniques run against the state explosion problem that is accentuated by the fact that the diamond property is difficult to meet, even for conflict-free transitions. To deal with this limitation, the partial order reduction (POR) techniques of Petri nets (PN for short) are used in combination with the partially ordered sets (POSETs). Nevertheless, POSETs introduce extra selection conditions that may offset the benefits of the POR techniques. This paper establishes a subclass of TPN for which the POR techniques of PN can be used without resorting to POSETs.