  Finite turn-based safety games have been used for very different problems
such as the synthesis of linear temporal logic (LTL), the synthesis of
schedulers for computer systems running on multiprocessor platforms, and also
for the determinisation of timed automata. In these contexts, games are
implicitly defined, and their size is at least exponential in the size of the
input. Nevertheless, there are natural relations between states of arenas of
such games. We first formalise the properties that we expect on the relation
between states, thanks to the notion of alternating simulation. Then, we show
how such simulations can be exploited to (1) improve the running time of the
OTFUR algorithm to compute winning strategies and (2) obtain a succinct
representation of a winning strategy. We also show that our general theory
applies to the three applications mentioned above.
