M.V. Iordache, J.O. Moody, and P.J. Antsaklis
Technical Report isis-2000-003, Department of Electrical
Engineering, University of Notre Dame, May 2000.
Abstract -- Given an arbitrary Petri net structure, which
may have uncontrollable and unobservable transitions, the
deadlock prevention procedure presented here determines a set of
linear inequalities on the marking of a Petri net. When the Petri
net is supervised so that its markings satisfy these inequalities,
the supervised net is proved to be deadlock-free for all initial
markings that satisfy the supervision constraints. Deadlock-freedom
implies that there will always be at least one transition that is
enabled in the closed loop (supervised) system. The method is not
guaranteed to insure liveness, as it can be applied to systems
that cannot be made live under any circumstances. However, it is
shown that when the method does insure liveness, it is at least
as permissive as any other liveness-insuring supervisor. Moreover,
it is shown that the method is not too restrictive even for Petri
nets in which not all transitions can be made live. The procedure
allows automated synthesis of the supervisors. Based on this
method we formulate and prove two extended methods with
guaranteed termination and a method for maximally permissive
deadlock prevention. The sufficient conditions for which our
theoretical results are guaranteed to apply can also be
automatically verified.
Technical Report [pdf file]
A shorter version of this technical report has been submitted for
journal publication.
Journal Submission [pdf file]