*For the most recent entries see the
Petri Nets Newsletter.*

## Proving non-reachability by modulo-place-invariants.

Desel, Jörg;
Radola, Micaela-Daphne
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.

*Do you need a refined search? Try our search engine
which allows complex field-based queries.*
*Back to the Petri Nets Bibliography*