Determining the reachability of an arbitrary marking is one of the interesting, but also one of the most difficult problems of elementary system nets. How to decide whether a marking
of an elementary system net
is reachable (from the initial marking
)? If only a finite number of markings is reachable, it is possible to construct each of them and test whether
is among them. If
is reachable, it is also possible to incrementally construct the (possibly infinite) marking graph until
is eventually encountered.
However, if an infinite number of markings is reachable in
is not one of them, then this procedure fails. Nevertheless, the problem can be solved: it is possible to construct a finite set
of reachable markings of
is reachable if and only if
is an element of
. However, this set is incredibly large and it was a long time before the reachability problem was solved.
In this chapter, we will discuss a necessary condition for the reachability and thus a sufficient condition for the unreachability of a marking. At the same time, we will formulate criteria for deciding whether a finite or an infinite number of markings are reachable.
To do this, we will add the
to our set of linear-algebraic tools. The covering graph, too, yields criteria for the reachability of markings and for the finiteness of the set of reachable markings.