With Paul Gastin, I mainly worked on graph based approaches for the analysis of timed systems. In particular, we looked at the model of timed push down automata (TPDA) and showed that behaviours of TPDA are graphs with a bounded tree width. Using this, we explicitly worked on constructing a tree automaton which accepts graphs which give rise to accepting behaviours of the TPDA.
With Patricia Bouyer-Decitre, I was looking at stochastic timed games (STGs). These are games played on timed automata where the probability distributions are decided based on the time constraints. We were specifically trying to prove the decidability of qualitative reachability in the case of 1-clock STG with 2 players. We have some preliminary ideas on which we are working on.