ANALYSIS OF SAFENESS, LIVENESS AND PERSISTENCE PROPERTIES OF PETRI NETS BY MEANS OF MONOTONE LOGIC FUNCTIONS

In the paper a new method of analysis of safeness, liveness and persistence properties of Petri nets is presented. This method is based on hierarchical representation of the state space of a Petri net by means of a collection of monotone logical functions and with related set of binary decision diagrams. The algorithm of symbolic analysis of a Petri net based behavioural specification of logic controllers is given, together with conditions, which allow analysing the properties mentioned above. One of the advantages of the proposed method is a possibility of detail analysis of selected local parts of a Petri net, as well as hierarchical approach for constructing the total state space.