Supervisory Controller Design to Enforce Basic Properties in Timed-Place Petri Nets

Supervisory controller design to enforce boundedness, reversibility, and liveness in discrete-event systems with time-delays is considered. It is assumed that the system is modeled by a timed-place Petri net. The approach of place-stretching, which has been introduced recently, is used for the purpose of designing a controller. Algorithms are presented to design a supervisory controller to enforce boundedness and reversibility simultaneously. This controller also guarantees T-livenees for the largest possible subset T of the set of transitions. Therefore, boundedness, reversibility, and liveness are enforced simultaneously whenever possible. Furthermore, the designed controller is also maximally permissive.