In: Valette, R.: Lecture Notes in Computer Science, Vol. 815; Application and Theory of Petri Nets 1994, Proceedings 15th International Conference, Zaragoza, Spain, pages 199-218. Springer-Verlag, 1994.
Abstract: This paper introduces two new kinds of invariant relation s based on the Petri net structure and the already proved invariant properties. These invariants establish a relation between the marking of two place subsets A and B: Exclusive Invariant states that A and B cannot be simultaneously marked, Implication Invariant states that when A is marked, B is also marked. In order to show the applicability of the presented invariants to be validation of models, we apply these invariants to the validation of two classical distributed algorithms: alternate bit protocol and Peterson's algorithm for n processes