PN: Formalism Presentation
Petri Nets: Formal Presentation
A transition t i is live for an initial marking M0 if for every
reachable marking M i, a firing sequence S from Mi
exists, which contains transition ti .
Interpretation: No matter what marking has been reached
from M0 , it is possible to ultimately fire any transition of
A Petri Net is live for M0 if all its transitions are live