M. V. Iordache, J. O. Moody, and P. J. Antsaklis
In the Proceedings of the 2001 American Control Conference, pp.4943-4948, June 2001.
Abstract -- Given an arbitrary Petri net structure which may have uncontrollable and unobservable transitions and may be unbounded, the procedure described in this paper generates a supervisor for liveness enforcement. The supervisor is specified as a conjunction of linear marking inequalities. For all initial markings satisfying the linear marking inequalities, the supervised Petri net is live. Moreover, the supervision is least restrictive in the fully controllable and observable case.
Slides available: [pdf, 85k]