Synthesising succinct strategies in safety and reachability games

Abstract

We introduce general techniques to compute, efficiently, succinct representations of winning strategies in safety and reachability games. Our techniques adapt the antichain framework to the setting of games, and rely on the notion of turn-based alternating simulation, which is used to formalise natural relations that exist between the states of those games in many applications. In particular, our techniques apply to the realisability problem of LTL [8], to the synthesis of real-time schedulers for multiprocessor platforms [4], and to the determinisation of timed automata [3] — three applications where the size of the game one needs to solve is at least exponential in the size of the problem description, and where succinct strategies are particularly crucial in practice.