  Considering real-valued clocks in timed automata (TA) makes it a practical
modeling framework for discrete-event systems. However, the infinite state
space brings challenges to the control of TA. To synthesize a supervisor for TA
using the conventional supervisory control theory, existing methods abstract TA
to finite automata (FA). For many applications, the abstraction of real-time
values results in an explosion in the state space of FA. This paper presents a
supervisory control synthesis algorithm directly applicable to the TA without
any abstraction. The plant is given as a TA with a set of uncontrollable events
and a set of forcible events. Forcible events can preempt the passage of time
when needed. The synthesis algorithm works by iteratively strengthening the
guards of edges labeled by controllable events and invariants of locations
where the progression of time can be preempted by forcible events. The
synthesized supervisor, which is also a TA, is guaranteed to be controllable,
maximally permissive, and results in a nonblocking and safe supervised plant.
