Marian V. Iordache, John O. Moody, and Panos J. Antsaklis
Technical Report isis-00-004, Dept. of Electrical Engr., Univ. of Notre Dame,
October 2000.
Abstract -- Given an arbitrary Petri net structure, which may have uncontrollable
and unobservable transitions, the liveness enforcement 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 live for all initial markings that satisfy
the supervision constraints. Also the supervision is proved to be maximally
permissive for a large class of Petri nets, which includes the fully controllable
and observable Petri nets. Moreover, the supervisor supports specifications
requiring only some of the Petri net transitions to be live. The maximal permissivity
typically applies also for this case. The procedure allows automated synthesis
of the supervisors. The sufficient conditions for which our theoretical results
are guaranteed to apply can be automatically verified.
Technical Report [pdf file]
A shorter version of this technical report has been submitted for journal publication.
Journal Submission [pdf file]