Deadlock prevention in flexible manufacturing systems: A verification-free resource configuration approach for liveness of finite-capacity S 3 PR

Deadlock prevention is a critical process in flexible manufacturing systems (FMSs) that ensures the smooth operation of the system and the efficient utilization of resources. A subclass of Petri nets (PNs) named System of Simple Sequential Process with Resources ( S 3 PR ) is a suitable formalism to model and analyze FMSs. The present study proposes a deadlock prevention approach that ensures the liveness of S 3 PR by calculating the minimum initial markings of resource places. First, an equivalent net of a finite-capacity S 3 PR has been constructed to describe its capacity function. Next, for the equivalent net, we prove some theorems on its initial markings of resource places under which the liveness of the equivalent net can be ensured. Finally, we develop an algorithm based on integer linear programming (ILP) and the proved theorems to ascertain the minimum necessary resources. Our developed approach can obtain a live net, and it does not need to check the liveness of the obtained marked PN. When compared with previous deadlock work, our approach reduces both facility costs and computational burden. Experimental results on FMSs are provided to validate the effectiveness of the proposed approach.