E. Asarin, O. Maler, A.Pnueli, J. Sifakis Controller
Synthesis for Timed Automata. In this work we tackle the
following problem: given a timed automaton, restrict its
transition relation in a systematic way so that all the remaining
behaviors satisfy certain properties. This is an extension of the
problem of controller synthesis for discrete event dynamical
systems, where in addition to choosing among actions, the
controller have the option of doing nothing and let the time pass.
The problem is formulated using the notion of a real-time game,
and a winning strategy is constructed as a fixed-point of an
operator on the space of states and clock configurations. [Postscript]