Two-player zero-sum games are a well-established model for synthesising
controllers that optimise some performance criterion. In such games one player
represents the controller, while the other describes the (adversarial)
environment, and controller synthesis corresponds to computing the optimal
strategies of the controller for a given criterion. Asarin and Maler initiated
the study of quantitative games on (non-probabilistic) timed automata by
synthesising controllers which optimise the time to reach a final state.