So far, timed automata have been studied and successfully applied mainly to classical verification problems, i.e. to check that a timed automaton satisfies a given logical requirement or to establish behavioural equivalences between timed automata. The class of problems to be treated in this project calls rather for synthesis problems: find a (dynamic) scheduler that achieves certain performance. Representing control problems in this framework leads to equation solving problems: the controller (i.e., the dynamic scheduler) appears as the unknown component that composed with the uncontrolled behaviour yields the desired behaviour. Using another terminology, the interaction between the scheduler and the rest of the system can be viewed as a two-player game where a winning strategy determines a scheduler which achieves the best possible results in the presence of uncontrolled uncertainty.

It has already been shown by members of the consortium that the controller synthesis problem can be posed and solved, in principle, for arbitrary timed automata. However there are many aspects which are specific to scheduling and resource allocation problems which need to be explored. In particular, finding a meaningful way to compare schedulers by criteria other than their worst-case performance is needed in order to evaluate solutions for the problem of job-shop under uncertainty. Other problems to be investigated are related to adapting control synthesis to distributed decision making situations where decisions should be based on partial information. Such problems have been treated in the past in the context of (untimed) discrete event systems but the problem they raise in timed systems are more difficult, for example, what information does one ``agent'', modeled as a timed automaton, know about the clock values of another agent, and whether it can use auxiliary clocks in order to infer the missing information.

responsible partner: VERIMAG