PN: Formalism Presentation
Petri Nets: Formal Presentation
From the initial marking M0, define all the enabled transitions and the next markings, if one of them is strictly greatest than M0, put w for each of the greatest components,
It exists a path M0Mi with a marking Mj = Mi, then stop for Mi,
Else, continue to built the successors of Mi ,
For each successor Mk of Mi,
a- a component of MI with w remains with w for Mk,
b- If it exists a marking Mj in the path M0Mk such as Mk>Mj then put w to all the greatest components.
The coverability tree is always finite