PN: Formalism Presentation
Petri Nets: Formal Presentation
The set of reachable marking from M is denoted A( R, M)
A marking M is reachable from a marking M 0 if there exists
a sequence of firings s Î T* that transforms M to M’.
A( R, M) is the Reachability tree of the net
Building the Reachability Tree
Create a tree where the nodes represent the reachable
markings and the arcs represent the transition firings.
Stop the expansion of a node in the tree if the node already