Solving games played on timed automata is a well-known problem and has led to tools and industrial case studies. In these games, the first player (Controller) chooses delays and actions and the second player (Perturbator) resolves the non-determinism of actions. However, the model of timed automata suffers from mathematical idealizations such as infinite precision of clocks and instantaneous synchronization of actions. To address this issue, we extend the theory of timed games in two directions. First, we study the synthesis of robust strategies for Controller which should be tolerant to adversarially chosen clock imprecisions. Second, we address the case of a stochastic perturbation model where both clock imprecisions and the non-determinism are resolved randomly. Finally we present a notion "repair" where we explain how to recover robustness in non-robust systems.

Short Bio:

Dr. Oualhadj is interested in algorithmic game theory and its application to verification and synthesis. He is a senior lecturer in the Computer Science Department of Université Paris-Est Créteil Val de Marne and also a member of the Specification and Verification of Systems team in the Logic, Algorithms, and Complexity Laboratory (LACL).

From November 2013 to August 2014, he held a postdoctoral position in the Computer Science Institute of Mons University (UMons) in the Theoretical Computer Science team led by Véronique Bruyère. From October 2012 to September 2013, he held a postdoctoral position in the MoVe team (LIF) within the project ECSPER at Aix Marseille University. For his PhD thesis, he worked under the supervision of Anca Muscholl and Hugo Gimbert on stochastic games.