# What the State is, and Where it comes from, when Generating Reachability Graphs

For Timed Automata, I found Figure 1 below. For Coloured Petri Nets I found Figure 2. Both are for "Reachability Graph Construction".

However, they don't describe where they got the states from (Figure 3), for generating the reachability graph. They assume you have "states" to generate a reachability graph, but I'm not sure what these states are. In the timed automata case, I'm not sure the automata "states" are what they are describing, it seems like by "state" they mean the program state after the automata runs (or on each step). Likewise for Petri nets, the state isn't the place or the transition, but the program state. At least that's what I'm getting.

Given that, my question is how to construct the program state, so that I can then construct the reachability graph. In addition, I'm wondering what the states actually are composed of. What the state is (boolean predicates, temporal logic expressions, data, etc.).

Some more detail. From here (on Petri nets):

A marking $M'$ is reachable from a marking $M$ if $M[s\rangle M'$ for some $s \in T^*$... The reachability set Reach(N) of N is the set of all markings that are reachable from the initial marking. [The markings have to do with the data associated to a place (a Petri net node)]... A Petri net $N = (P, T, F, M_0)$ induces several standard structures on which first-order logics may be interpreted... To specify properties of structures ... obtained from a Petri net $N$, we introduce a first-order logic FO with atomic predicates $x \to y$, $x \overset{*}{\to} y$, $x \overset{+}{\to} y$ and $init(x)$. [Then they go into the model checking part].

That just demonstrates how the Reachability Graph Construction is left out. That is, what it is composed of (in some detail), and how to construct it.

Figure 1 $\downarrow$ Figure 2 $\downarrow$ Figure 3 $\downarrow$ Petri net case: In the Petri net case, the states are the possible markings of the network. Note that the state set could be finite or infinite depending on the network. In paper that you referenced ("Petri Net Reachability Graphs: Decidability Status of First Order Properties" by Philippe Darondeau, Stéphane Demri, Roland Meyer, Christophe Morvan), the reachability graph is defined on page 4 as consisting of all markings and having a transition between a marking $M$ and $M'$ if we have $M[t\rangle M′$ some $t$. This notation is in turn explained at the beginning of the page, in Definition 2.