Oded Maler (CNRS-Verimag), Controller Synthesis with Adversaries

Many problems in numerous domains related to the design and analysis of systems can be seen, if looked at through an appropriate abstraction, as variations and special cases of one fundamental problem, namely the problem of finding a strategy in a two-player dynamic game. In this game, player I is the "controller", the system that we design, and player II is the "environment" that generates events beyond our control. Variants of this problem differ from each other by the nature of the state space and time domain on which the game is defined (discrete, continuous, timed, hybrid), by the classes of cost function (additive over time, discrete), and by the way the outcome is quantified over the actions of the adversary (worst case, average case).

In this talk I will sketch a generic model for this problem whose instances include verification by model-checking, optimal and model-predictive control, AI planning and game playing, Markov decision processes, scheduling and more. I will identify three classes of techniques which are commonly-used for computing solutions:

1) Restriction to a finite time horizon and reduction to a constrained optimization problem (SAT, LP, mixed) 2) Backward value iteration (dynamic programming, fix point computation, HJB) 3) Heuristic forward search in the space of partial strategies.

In the second part of the talk I will sketch some work on one instance of this scheme, the problem(s) of scheduling under uncertainty, where the controller is a scheduler, allocating resources to tasks and the environment may dynamically affect task specifications, task durations or resource availability. I will show how such situations can be modelled naturally using timed automata and, sometimes, be solved algorithmica