Proving nonreachability by modulo-invariants

We introduce modulo-invariants of Petri nets which are closely related to classical place-invariants but operate in residue classes module k instead of natural or rational numbers. Whereas place-invariants prove the nonreachability of a marking if and only if the corresponding marking equation has no solution in Q, a marking can be proved nonreachable by modulo-invariants if and only if the marking equation has no solution in Z. We show how to derive from each net a finite set of invariants - containing place-invariants and modulo-invariants - such that if any invariant proves the nonreachability of a marking, then some invariant of this set proves that the marking is not reachable.