On commoner's 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, although not necessarily immediately. A free-choice Petri net (FCPN) is a PN, where every are from a place to a transition is either the unique output are from that place or it is the unique input are to the transition. Commoner's Liveness Theorem (cf. Hack, 1972, Ch. 4; Reisig, 1985, Section 7.2) states that a FCPN is live if and only if every siphon 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 . subset of or equal to . P). We concern ourselves with marking-dependent supervisory policies that can prevent the tiring of a transition. We characterize supervisory policies that enforce liveness in non-live FCPNs using observations that strongly parallel Commoner's Liveness Theorem. We use this characterization to establish the existence of supervisory policies that enforce liveness in a Class of FCPNs called independent, increasing free-choice petri nets (II-FCPNs). (C) 1997 Elsevier Science B.V.