Most permissive liveness-enforcing Petri net supervisors for discrete event systems via linear monitors

Xuya Cong; Anrong Wang; Yufeng Chen; Naiqi Wu; Ting Qu; Mohamed Khalgui; Zhiwu Li

doi:10.1016/j.isatra.2019.02.003

Most permissive liveness-enforcing Petri net supervisors for discrete event systems via linear monitors

ISA Trans. 2019 Sep:92:145-154. doi: 10.1016/j.isatra.2019.02.003. Epub 2019 Feb 15.

Authors

Xuya Cong¹, Anrong Wang², Yufeng Chen³, Naiqi Wu⁴, Ting Qu⁵, Mohamed Khalgui⁶, Zhiwu Li⁷

Affiliations

¹ School of Electro-Mechanical Engineering, Xidian University, No. 2 South Taibai Road, Xi'an 710071, China; Department of Electrical and Information Engineering, Polytechnic of Bari, 70125 Bari, Italy. Electronic address: congxuya@163.com.
² School of Electro-Mechanical Engineering, Xidian University, No. 2 South Taibai Road, Xi'an 710071, China. Electronic address: arwang@mail.xidian.edu.cn.
³ Institute of Systems Engineering, Macau University of Science and Technology, Macau. Electronic address: chyf01@163.com.
⁴ Institute of Systems Engineering, Macau University of Science and Technology, Macau. Electronic address: nqwu@must.edu.mo.
⁵ School of Intelligent Systems Science and Engineering, Jinan University (Zhuhai Campus), Zhuhai, 519070, China. Electronic address: quting@jnu.edu.cn.
⁶ School of Intelligent Systems Science and Engineering, Jinan University (Zhuhai Campus), Zhuhai, 519070, China. Electronic address: khalgui.mohamed@gmail.com.
⁷ Institute of Systems Engineering, Macau University of Science and Technology, Macau; School of Electro-Mechanical Engineering, Xidian University, No. 2 South Taibai Road, Xi'an 710071, China. Electronic address: zhwli@xidian.edu.cn.

PMID: 30850206
DOI: 10.1016/j.isatra.2019.02.003

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.

Keywords: Behavioural permissiveness; Deadlock prevention; Discrete event system; Petri net; Supervisory control.