We are interested in tools for synthesizing strategies in timed games with parity objective.

From a theoretical point of view, we define and interpret these games as in the paper The Element of Surprise by Luca de Alpharo et al. (CONCUR 2003). This paper highlights several subtleties of timed games. They can be summarized as follows: representing a timed parity game by an interleaving of waiting steps (continuous transition) and actions (discrete transition) does not capture the strategies that require to be the fastest (as in a cowboy duel). Such strategies are called surprise strategies and do not have equivalent no-surprise strategies. Thus, taking surprise into account changes the game, i.e., the winner may be different depending on whether we consider surprise strategies.

To our knowledge, the results of this paper have not been implemented in concrete tools. The paper does not propose an explicit construction or other implementation methods, and UppAal, a well-known timed game solver, considers a different semantics and focuses on reachability and safety objectives.

We therefore propose an explicit construction corresponding to the work of de Alpharo et al. and present its use in Zielonka’s procedure for solving timed parity games. We believe that a tool for experimenting with new semisymbolic algorithms on timed games would benefit the community.

TChecker is a project built in this sense and is in active development for at least eight years. However, it is a model checker: it does not yet support games. Therefore,
together with Gilles Geeraerts* , Jean-François Raskin* , and Frédéric Herbreteau** , we are working on integrating game support into TChecker and implementing our timed Zielonka’s algorithm there as a proof of concept.

* Université Libre de Bruxelles
** Bordeaux INP / LaBRI