ON COMMONERS LIVENESS THEOREM AND SUPERVISORY POLICIES THAT ENFORCE LIVENESS IN FREE-CHOICE PETRI NETS

A Petri net (PN) (Peterson, 1981; Reisig, 1985) is said to be live if it is possible to fire any transition from every reachable marking, al though not necessarily immediately. A free-choice Petri net (FCPN) is a PN, where every are from a place to a transition is either the uniqu e output are from that place or it is the unique input are to the tran sition. Commoner's Liveness Theorem (cf. Hack, 1972, Ch. 4; Reisig, 19 85, Section 7.2) states that a FCPN is live if and only if every sipho n contains a marked trap at the initial marking. A siphon (trap) is a collection of places P such that . P subset of or equal to P . (P . su bset of or equal to . P). We concern ourselves with marking-dependent supervisory policies that can prevent the tiring of a transition. We c haracterize supervisory policies that enforce liveness in non-live FCP Ns using observations that strongly parallel Commoner's Liveness Theor em. We use this characterization to establish the existence of supervi sory policies that enforce liveness in a Class of FCPNs called indepen dent, increasing free-choice petri nets (II-FCPNs). (C) 1997 Elsevier Science B.V.