On a free-choice equivalent of a Petri net

A Petri net (PN) is said to be live if it is possible to fire any transition from every reachable marking, although not necessarily immediately. In this paper we consider the issue of enforcing liveness in nonlive PNs via supervisory control. Using a construction procedure that converts an arbitrary PN into an equivalent member of a family of PNs called free-choice Petri nets, we show there is a policy that enforces liveness in the original PN if and only if there is a corresponding policy for its free-choice equivalent. The utility of this approach is illustrated via an example