Reachability in Elementary System Nets

Chapter

Abstract

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 M of an elementary system net N is reachable (from the initial marking M 0)? If only a finite number of markings is reachable, it is possible to construct each of them and test whether M is among them. If M is reachable, it is also possible to incrementally construct the (possibly infinite) marking graph until M is eventually encountered.

However, if an infinite number of markings is reachable in N, and M is not one of them, then this procedure fails. Nevertheless, the problem can be solved: it is possible to construct a finite set K of reachable markings of N such that M is reachable if and only if M is an element of K. 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 marking equation and transition invariants 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.