A method for the synthesis of liveness enforcing supervisors in Petri nets

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.