TY - JOUR
T1 - Structural Liveness Analysis of Automated Manufacturing Systems Modeled by S4PRs
AU - Feng, Yanxiang
AU - Xing, Keyi
AU - Zhou, Meng Chu
AU - Tian, Feng
AU - Liu, Huixia
N1 - Funding Information:
Manuscript received November 25, 2018; accepted February 19, 2019. Date of publication April 11, 2019; date of current version October 4, 2019. This paper was recommended for publication by Associate Editor E. Roszkowska and Editor S. Reveliotis upon evaluation of the reviewers’ comments. This work was supported in part by the National Natural Science Foundation of China under Grant 61573278, Grant 61304052, and Grant 61877048, in part by the National Science Foundation for Post-Doctoral Scientists of China under Grant 2018M643660, and in part by the Shandong Provincial Natural Science Foundation of China under Grant ZR2018MF024. (Corresponding author: Keyi Xing.) Y. Feng, K. Xing, and F. Tian are with the State Key Laboratory for Manufacturing Systems Engineering, Systems Engineering Institute, Xi’an Jiaotong University, Xi’an 710049, China (e-mail: fengyxss@stu.xjtu.edu.cn; kyxing@mail.xjtu.edu.cn; fengtian@mail.xjtu.edu.cn).
Publisher Copyright:
© 2019 IEEE.
PY - 2019/10
Y1 - 2019/10
N2 - This paper presents a liveness analysis method for sequential automated manufacturing systems (AMSs), which can be modeled by a class of Petri nets named systems of sequential systems with shared resources (S4PR). We show that deadlocks in S4PR can be characterized by the saturation of its structural object named a perfect activity circuit (PA-circuits). Thus, S4PR is live if and only if no PA-circuits in it is saturated at all reachable states. A PA-circuits of an S4PR may not be saturated at any state; hence, we propose an integer linear program (ILP) to determine whether a PA-circuits can be saturated or not. Then an algorithm is proposed to compute the set of PA-circuits that may be saturated. This presented method nontrivially generalizes deadlock characterization and liveness condition of ordinary Petri nets to a broader class of nonordinary ones.Note to Practitioners-In the context of AMS, liveness is the most important property since it implies that there is no partial deadlock during the system evolution, and hence, all part types can be produced smoothly. We study the problem of liveness for AMS with the most general resource allocation and flexible routing, which can be modeled by S4PRs or disjunctive/conjunctive (D/C) resource allocation systems (RASs). Given such a complex AMS, based on its Petri net model, this paper presents a sufficient and necessary liveness condition by utilizing the structural properties, and develops an algorithm to identify all the structural objects that may lead the systems to deadlocks. This paper is significant in liveness-enforcing supervisor design for S4PR.
AB - This paper presents a liveness analysis method for sequential automated manufacturing systems (AMSs), which can be modeled by a class of Petri nets named systems of sequential systems with shared resources (S4PR). We show that deadlocks in S4PR can be characterized by the saturation of its structural object named a perfect activity circuit (PA-circuits). Thus, S4PR is live if and only if no PA-circuits in it is saturated at all reachable states. A PA-circuits of an S4PR may not be saturated at any state; hence, we propose an integer linear program (ILP) to determine whether a PA-circuits can be saturated or not. Then an algorithm is proposed to compute the set of PA-circuits that may be saturated. This presented method nontrivially generalizes deadlock characterization and liveness condition of ordinary Petri nets to a broader class of nonordinary ones.Note to Practitioners-In the context of AMS, liveness is the most important property since it implies that there is no partial deadlock during the system evolution, and hence, all part types can be produced smoothly. We study the problem of liveness for AMS with the most general resource allocation and flexible routing, which can be modeled by S4PRs or disjunctive/conjunctive (D/C) resource allocation systems (RASs). Given such a complex AMS, based on its Petri net model, this paper presents a sufficient and necessary liveness condition by utilizing the structural properties, and develops an algorithm to identify all the structural objects that may lead the systems to deadlocks. This paper is significant in liveness-enforcing supervisor design for S4PR.
KW - Automated manufacturing system (AMS)
KW - Petri nets
KW - liveness analysis
KW - resource allocation systems (RAS)
UR - http://www.scopus.com/inward/record.url?scp=85064604890&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85064604890&partnerID=8YFLogxK
U2 - 10.1109/TASE.2019.2905277
DO - 10.1109/TASE.2019.2905277
M3 - Article
AN - SCOPUS:85064604890
SN - 1545-5955
VL - 16
SP - 1952
EP - 1959
JO - IEEE Transactions on Automation Science and Engineering
JF - IEEE Transactions on Automation Science and Engineering
IS - 4
M1 - 8688640
ER -