Macro liveness graph and liveness of ω -independent unbounded nets

Liveness is a basic property of a system and the liveness issue of unbounded Petri nets remains one of the most difficult problems in this field. This work proposes a novel method to decide the liveness of a class of unbounded generalized Petri nets called ω -independent unbounded nets, breaking the existing limits to one-place-unbounded nets. An algorithm to construct a macro liveness graph (MLG) is developed and a critical condition based on MLG deciding the liveness of ω -independent unbounded nets is proposed. Examples are provided to demonstrate its effectiveness.