Liveness Analysis of Petri Nets Using Siphons and Mathematical Programming

Liveness is a significant behavioral property of a Petri net. Siphons, as structural objects, are closely related to the liveness of a Petri net. For generalized systems of simple sequential processes with resources (GS3PR), a mixed integer programming (MIP) model is formulated, which can detect the existence of minimal non-max*-marked siphons that cause deadlocks or livelocks. We conclude that a GS3PR is live if there is no feasible solution to the formulated MIP model. An example is used to illustrate the proposed method.