Verifying Time Petri Nets by Linear Programming

The paper proposes an approach to solving some verification problems of timePetri nets using linear programming. The approach is based on theobservation that for loop-closed time Petri nets, it is onlynecessary to investigate a finite prefix of an untimed run of theunderlying Petri net. Using the technique the paper gives solutions toreachability and bounded delay timing analysis problems. For bothproblems algorithms are given, that are decision procedures forloop-closed time Petri nets, and semi-decision procedures for generaltime Petri nets.