Nonblocking control of Petri nets using unfolding

We deal with the problem of controlling a safe place/transition nets so as to avoid a set of forbidden markings F. If a given set of markings has property REACH, i.e., if it is closed under the reachabilityoperator, we have shown that using the technique of unfolding is possible to efficiently design a maximally permissive supervisor to solve this control problem. The supervisor takes the form of a set of control places to be added to the unfolding of the original net.In this paper we consider the additional problem of forbidding a larger set F_I that also contains those markings from which a marking in F is inevitably reached unless the controller introduces adeadlock and show how this problem can be solved still using the unfolding.