Online seminar) Timed games and deterministic separability

The presentation is based on my recent joint work with Lorenzo Clemente and
Sławomir Lasota. We study a generalisation of Büchi-Landweber games to the
timed setting, where Player I plays timed actions and Player II replies immediately
with untimed actions. The winning condition is specified by a non-deterministic timed
automaton for Player I.

I will sketch a proof of our result that for each K it is decidable whether Player II
has a winning timed controller using K clocks. As an application of timed games,
I will show that they can be used to solve the deterministic separability problem
for nondeterministic timed automata.