On supervisory policies that enforce liveness in completely controlled Petri nets with directed cut-places and cut-transitions

The process of synthesizing a supervisory policy that enforces liveness in a Petri net (PN), where each transition can be prevented from firing by an external agent, can be computationally burdensome in general. In this paper we consider PN's that have a directed cut-place or a cut-transition. A place (transition) in a connected PN is said to be a cut-place (cut-transition) if its removal will result in two disconnected component PN's. A cut-place is said to be a directed cut-place, if in the original PN, all arcs into this cut-place emanate from transitions in only one of the two disconnected component PN's. The authors show there is a supervisory policy that enforces liveness in the original PN if and only if similar policies exist for two PN's derived from the disconnected components obtained after the removal of the directed cut-place (cut-transition). The utility of this observation in alleviating the computational burden of policy synthesis is illustrated via example.