Timed synthesis games

We study a generalisation of Büchi-Landweber games to the timed setting with an aim of solving the strategy synthesis problem for Player II. In our setting, that equals to constructing a timed automaton with an output – a timed controller. We show that for fixed number of clocks but *without* specifying the maximal numerical constant available to Player II, it is decidable whether she has a winning timed controller using these resources. This is an important technical novelty, since the related decidability results found in previous literature required both constants to be fixed. As an application of timed games, we show that they can be used to solve the deterministic separability problem for nondeterministic timed automata. This is a novel decision problem about timed automata which has not been studied before. During the presentation, I will briefly introduce our games and show, how our results can be used to solve the separability problem. This presentation is based on a paper by Lorenzo Clemente, Sławomir Lasota, and Radosław Piórkowski.

Authors

• Radosław Piórkowski

Keywords

No keywords are indexed for this paper.