Structural Liveness Analysis of Automated Manufacturing Systems Modeled by S⁴PRs

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 (S⁴PR). We show that deadlocks in S⁴PR can be characterized by the saturation of its structural object named a perfect activity circuit (PA-circuits). Thus, S⁴PR is live if and only if no PA-circuits in it is saturated at all reachable states. A PA-circuits of an S⁴PR 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 S⁴PRs 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 S⁴PR.