Synthesis of Real-Time Systems

system is correct. While verification requires the programmer to provide both
the specification and the implementation, synthesis automatically transforms
the specification into an implementation that is correct by construction.

Synthesizing an implementation of a reactive system corresponds to solving an
infinite two-player game. In this talk, I will give an overview on
game-theoretic algorithms for the synthesis of real-time controllers. I will
present a novel technique for the reduction of timed games that, based on a
local analysis of the game tree, determines if a particular move will not
change the outcome of the game and can therefore safely be ignored. I will
conclude with examples from the synthesis of industrial controllers.