Insufficiently marked siphon of Petri nets - extension of token-free siphon
Akinori Ohta, Kohkichi Tsuji · 2003
Petri net is a mathematical model for concurrent systems. Liveness is one of important properties of Petri net. A live Petri net exhibits no local deadlocks. Siphon is a subset of places useful for liveness analysis. Token-free siphon implies non-liveness of Petri net. In this report, we suggest an insufficiently marked siphon as an extended token-free siphon. More general necessary condition for liveness is obtained using this new status of siphons. Two methods are proposed to obtain an insufficiently marked siphon.