Reachability Graph
This is a way of representing the states of Petri Nets
A marking $M$ is reachable from the initial marking $M_0$
 $\iff M_0 \to^* M$
 i.e. there exists a firing sequence that brings us from the initial state of a petri net to a state that corresponds to $M_0$
In a reachability graph of a petri net $N = (P, T, F)$
 nodes correspond to reachable markings
 edges correspond to the relation $\to$
There can be several notations for markings:
 first one: $(n_1, n_2, ..., n_m)$ corresponds to the number of elements in the places $(p_1, ..., p_m)$ respectively
 second one: $[p_1^{n_1}, ..., p_m^{n_m}]$ where $n_i$ is the number of times $p_i$ appears
 if $p_i$ appears zero times, we don't show it in the marking
Consider this example:

 so a reachability graph shows all possible states (markings) that you can reach by triggering transitions that are enabled

 the graph above is the reachability graph with different notation
There are some desirable properties for the Workflow Nets
 we want to be able to decide on them
 reachability graphs can be used for that
This is a similar notion for expressing states of Workflow Nets
 but unlike Reachability Graph it can be finite for unbounded nets
 yet in many cases less expressive
Examples
Example 1

 it is a reachability graph for

 we see that two nodes are not connected: it's clearly a problem
Sources