Two-player games allow to model systems that interact with their environment. Timed games further take into account real-time constraints[1]. A player wins the game when some condition is met: reachability of a state, avoiding some state (safety), Büchi accepting condition, etc. The goal of the system is to win the (timed) game independently of the actions performed by the environment.
A winning strategy defines the sequence of delays and actions that the system should take in order to win the game. However, not all strategies are suitable to real-time systems. Every stategy that requires to play an infinite number of actions within a finite amout of time is obviously not realistic. Such strategies are called Zeno strategies.
Non-Zenoness can be ensured by adding an extra Büchi condition to the game. A first solution has been proposed in[2]. However, it has been shown that this approach can lead to an exponential blowup[3]. A better solution has been proposed in[3,4]. The goal of this internship is to study how the latter can be used to synthesize non-Zeno strategies for timed games.
Timed games have an infinite (and even uncountable) state space. Hence, synthesis algorithms use finite abstractions of the game. For efficiency reasons, we are interested in zone-based abstractions rather than the region abstraction. The algorithm in[5] is a zone-based algorithm for reachability and safety timed games. The starting point of internship is to study how the solution in[3,4] can be combined with the algorithm in[5] to synthesize non-Zeno startegies for timed games.