A transition t is L2-live if for any positive finite integer k, there exists a firing sequence from M₀ which fires t k times.
Strict L2-liveness implies non-L3-liveness: there exists NO infinite firing sequence from M₀ which fires t infinitely many times.
SCC analysis of the state space enables us to detect L3 and L4, but It is not clear to me how to detect L2.
A transition
tis L2-live if for any positive finite integerk, there exists a firing sequence fromM₀which firestktimes.Strict L2-liveness implies non-L3-liveness: there exists NO infinite firing sequence from
M₀which firestinfinitely many times.SCC analysis of the state space enables us to detect L3 and L4, but It is not clear to me how to detect L2.