Most permissive liveness-enforcing Petri net supervisors for discrete event systems via linear monitors. (September 2019)

• Record Type: Journal Article
• Authors: Cong, Xuya; Wang, Anrong; Chen, Yufeng; Wu, Naiqi; Qu, Ting; Khalgui, Mohamed; Li, Zhiwu
• Is Part Of: ISA transactions. Volume 92(2019)
• Page Start: 145
• Page End: 154
• Publication Date: 2019-09
• Subjects: Discrete event system -- Petri net -- Supervisory control -- Deadlock prevention -- Behavioural permissiveness; Engineering instruments -- Periodicals; Engineering instruments; Periodicals; Electronic journals; 629.805
• DOI: 10.1016/j.isatra.2019.02.003
• Languages: English
• ISSNs: 0019-0578

Abstract

Abstract: This paper proposes a deadlock prevention method to design a maximally permissive liveness-enforcing pure Petri net supervisor for a discrete event system, if such a supervisor exists; otherwise, it obtains the most permissive one in the sense that no other pure liveness-enforcing supervisors via linear monitors can be more permissive than it. This paper exploits an iterative method. At each iteration, a first-met bad marking (FBM) is singled out and an integer linear programming problem (ILPP) is configured. If a feasible solution can be found for the ILPP, then a place invariant (PI) is designed to prohibit the FBM from being reached while no legal marking is forbidden. If the ILPP has no solution, we collect all these FBMs that cannot be optimally controlled. For each of such FBMs, another ILPP is designed to find the least number of legal markings whose reachability conditions contradict the current considered FBM and enumerate all the optimal solutions of this ILPP. Based on it, we develop a 0–1 linear programming problem to find the maximal number of legal markings after removing all the contradictory legal markings. Then, the new sets of legal markings and FBMs are obtained, and we return to the iteration stage to redesign a PI to control each FBM if the ILPP has a feasible solution. Repeat the above process until no FBM can be reached. Finally, a most permissive pure liveness-enforcing supervisor via linear monitors is derived. Two Petri net models are used to illustrate the proposed method. Highlights: This paper designs an optimal pure net supervisor if such a supervisor exists. The control policy is an iterative process to obtain an optimal pure net supervisor. If optimal pure net supervisors do not exist, we design a most permissive supervisor. The proposed method is applicable for any bounded Petri nets.