A Petri Net Structure-Based Deadlock Prevention Solution for Sequential Resource Allocation Systems

A new method for the deadlock prevention problem in concurrent systems where a set of processes share a set of common resources in a conservative way is proposed. It can be applied to flexible manufacturing systems, modeled with Petri nets. In this paper, we present a set of important results related to the deadlock prevention problem in S⁴PR nets. First, a liveness characterization is introduced, establishing how deadlocks can be studied in terms of circular waits. Second, we show how a circular wait situation corresponds to a particular marking related to a siphon of the Petri net model. Finally, this last characterization is used to obtain an iterative method that successively forbids deadlock related states, synthesizing the control necessary to ensure a final live behavior. The method can be implemented by means of the solutions of a set of integer linear programming problems.