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

Question

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$

Answer 1

Timed automaton case: Here, a state is typically composed of the current location and the values of all clock variables. Thus, timed automata induce transition systems with an infinite number of states.

The usual approach in this context is thus to build a finite representation of this state set, which is a finite transition system. In the paper "An Efficient State Space Generation for Analysis of Real-time Systems" by Inhye Kang and Insup Lee that you linked to, the state set for this finite transition system is given on page 5, left column. The classical approach involves building a so-called region graph, which is referenced in column 2 of page 4.

Note that CTL model checking of the resulting transition system makes little sense, as the "next-time" operator of CTL does not have a usable semantic in this case. Rather, there are specialized logics (such as TCTL) to reason about properties of timed systems.

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.