On a Free-Choice Equivalent of a Petri Net

A Petri net (PN) [2, 3] 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 non-live PNs via supervisory control. Using a construction procedure, similar to that in reference [1], that converts an arbitrary PN into an equivalent member of a family of PNs called Free-Choice Petri nets (cf. section 7.2, [3]), 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. 1 Introduction A large class of systems can be modeled as systems with independent, interacting, concurrent components. Typically, each independent process is split into several operations, the execution of each operation is conditioned on the satisfaction of a set of logical preconditions. Upon the execution of any such operation, a new set of..