Structural Liveness Analysis of Automated Manufacturing Systems Modeled by S4PRs

Yanxiang Feng, Keyi Xing, Meng Chu Zhou, Feng Tian, Huixia Liu

Research output: Contribution to journalArticlepeer-review

12 Scopus citations


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.

Original languageEnglish (US)
Article number8688640
Pages (from-to)1952-1959
Number of pages8
JournalIEEE Transactions on Automation Science and Engineering
Issue number4
StatePublished - Oct 2019

All Science Journal Classification (ASJC) codes

  • Control and Systems Engineering
  • Electrical and Electronic Engineering


  • Automated manufacturing system (AMS)
  • Petri nets
  • liveness analysis
  • resource allocation systems (RAS)


Dive into the research topics of 'Structural Liveness Analysis of Automated Manufacturing Systems Modeled by S4PRs'. Together they form a unique fingerprint.

Cite this