Supervisory control of timed automata

Based on the framework of Ramadge and Wonham theory, this paper presents a methodology for the design of a supervisory control for timed discrete event systems. Timed automata in dense time domain are used as models. They are successively extended to region automata and τ-region automata in which passing of time is considered as an event, either controllable (tack), either uncontrollable (tock). An example illustrates the different steps for the design of the timed, complete and minimally restrictive supervisor.