New structural invariants for petri nets analysis

Abstract

This paper introduces two new kinds of invariant relations 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 lnvariant 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 the 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.