PN: Formalism Presentation
Petri Nets: Formal Presentation
A Petri Net is deadlock- free for M 0 if no reachable
A deadlock is a marking such that no transition is enabled.
When a model has a deadlock, the corresponding real system can block
- This property is weaker than the one of liveness,
it only implies that the network has always the possibility to evolve.
- liveness and dead-lock free are are two distinct notions.
A network can be deadlock-free and no of its