In: Thiagarajan, P.S.: Lecture Notes in Computer Science, Vol. 880; Proceedings of 14th Conference on the Foundations of Software Technology and Theoretical Computer Science, Madras, pages 366-377. Springer-Verlag, 1994.
Abstract: The reachability problem of Petri nets is the problem of deciding whether a marking can be reached from the initial marking by a sequence of occurrences of transitions. It is decidable in general, but it has a very high complexity. For proving that a given marking is not reachable, the technique of invariants can be used. The best known and most applied invariant properties are those derived from place-invariants. Formally, a place-invariant associates weights to the places of the net such that the weighted sum of tokens is not changed by the occurrence of transitions. We introduce modulo-place-invariants of Petri nets which are closely related to classical place-invariants but operate in residue-classes modulo k instead of rational or real numbers. Whereas classical place-invariants prove the non-reachability of a marking if and only if the corresponding marking-equation has no solution in Q, a marking can be proved non-reachable by modulo-place-invariants if and only if the marking-equation has no solution in Z. Thus, modulo-place-invariants properly generalize classical place-invariants.