In: Proc. IFAC Conf. on Control Systems Design (CSD'2000), 18-20 June 2000, Bratislava, Slovak Republic, pages 323-328. 2000.
Abstract: This paper presents necessary and sufficient conditions that verify the existence of liveness-enforcing supervisory policies for an n-safe ordinary Petri nets with uncontrollable transitions. The approach is based on a partial method called network unfolding, which unfolds the original net to an acyclic occurrence net. The occurrence net preserves the ordering relationship among transitions and enumerates all the reachable markings of the original network. A set of base configurations is identified from the occurrence net. A base configuration can be live or deadlocked. A set of base configurations may be in a cyclic lock. It is shown that there exists a liveness-enforcing supervisory policy if and only if every transition of the original net is contained in some live base configuration and every deadlocked base configuration as well as every cyclic lock is controllable. Furthermore, it is shown that the liveness-enforcing supervisory policy constructed in the sufficiency proof is maximally permissive (or minimally restrictive).
Keywords: Petri nets. occurrence nets, discrete-event systems, liveness-enforcing supervision, supervisory control, uncontrollable transitions.