Heuristics for efficient game solving

Recently, verification tools have experienced very important improvements in performance. These gains of performance are the result of a better understanding of classical verification problems, giving rise to efficient heuristics, and careful implementations using adequate data-structures.

We want to achieve comparable improvement in tool performance for synthesis, in the context of games for instance on timed automata. The UPPAAL-TIGA tool currently handles time optimal strategies and can output strategies for games with perfect information. We want to investigate more useful classes of games on timed automata to scale up the size of the models that we can handle, enable extensions such as costs and robustness, and obtain more useful code generation with respect to target controllers.