Semilinearity

In this chapter, the reachability graphs of – possibly unbounded – persistent Petri nets will be examined. It turns out that they, too, have a special structure. Even though the reachability sets of unbounded persistent nets contain infinitely many markings, it turns out that they are still semilinear. Semilinearity is a generalization of the notion of “ultimately periodic”, known for infinite words,1 to vectors of natural numbers. Semilinear sets are decidable, a fact which can be exploited in proving that persistence is decidable, too. Semilinearity is also related to a special logic on the natural numbers called Presburger logic.