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 (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-cir...