M. V. Iordache, J. O. Moody and P. J. Antsaklis
Technical report of the ISIS Group, ISIS-99-006, Department of Electrical Engineering, University of Notre Dame, July 1999.
Abstract -- Deadlock is the condition of a system that has reached a state in which all of its potential actions are blocked. This paper introduces a deadlock prevention method for discrete event systems modeled by Petri nets. Petri nets have a bipartite graph structure and they are particularly well suited to model concurrencies found in manufacturing, communication and computer systems, among others. Given an arbitrary Petri net structure, the deadlock prevention algorithm in this paper finds linear inequalities in terms of the marking (state vector). When the Petri net is supervised to satisfy the constraints provided by the algorithm, the supervised net is proved to be deadlock-free for all initial markings that satisfy the supervision constraints. Results pertaining to permissivity properties and termination are also proved. The algorithm is applicable to any Petri net with controllable and observable transitions.