Uppaal-Tiga: Timed Games for Everyone

In 2005 we proposed the first efficient on-the-fly algorithm for solving games based on timed game automata with respect to reachabil- ity and safety properties. Since then we have completely re-implemented the first prototype and made dramatic improvements both in terms of performance (several orders of magnitude) and the input language (com- plete support of all the language features of Uppaal). In addition, the tool supports the new feature of strategy generation with different com- pactness levels. In this paper we present this new version of Uppaal- Tiga.