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