Synthesis of Liveness Enforcing Supervisory Policies In Petri Nets by Stepwise Refinement

The refinement procedure of Suzuki and Murata [I] combines two Petri Nets (PNs) N-1(m(1)(0)) and N-2(m(2)(0)) in a prescribed manner to obtain a PN N-3(m(3)(0)). Under appropriate conditions, the liveness of the PNs N-1(m(1)(0)) and N-2(m(2)(0)) implies the liveness of the PN N-3(m(3)(0)). A PN that is nut live, can be made live by a liveness enforcing supervisory policv (LESP). In this paper, we develop the results of Suzuki and Murata to yield a class of PNs for which an LESP for N-3(m(3)(0)) can be represented in terms of local-LESPs for N-1(m(1)(0)) and N-2(m(2)(0)).