Synthesis of feedback control elements for discrete event systems using Petri net models and theory of regions

This paper describes a method for constructing a Petri-net-based controller for a discrete event system (DES) modelled by a Petri net. Assuming that an uncontrolled Petri net model of the DES and a set of forbidden state specifications are given, feedback control elements, i.e. a set of places and related transitions, with initial marking, are computed using the theory of regions, which is a formal synthesis technique for deriving Petri nets from automaton-based models. When feedback control elements are added to the uncontrolled Petri net model, the controlled (closed-loop) Petri net model of the system is obtained. The controlled Petri net model obtained is maximally permissive while guaranteeing that forbidden states do not occur. The proposed method is computationally efficient and does not suffer from the state explosion problem. Two examples are provided to show the applicability of the proposed method.