Control design for nondeterministic input/output automata

This paper presents a new control design approach for discrete-event systems described by Input/Output automata. A formal design method guarantees the fulfillment of the specifications for the closed-loop system including the system safety. Necessary and sufficient conditions for the well-posedness of the control loop and the controllability of the plant with respect to the specification are proved. The control of a batch process is used to illustrate the results.