PN: Formalism Presentation
Petri Nets: Formal Presentation
A place pi is bounded for an initial marking M0 if for all
markings reachable from M0 , M(pi)<= k (positive integer)
p is k- bounded Û " M Î A( R, M 0 ), M( p) £ k
A net is bounded for an initial marking M 0 if all places
are bounded for M 0 (similarly for k- bounded)
A net is safe iff it is 1- bounded