Automata-Theoretic Decision of Timed Games

The solution of games is a key decision problem in the context of verification of open systems and program synthesis. We present an automata-theoretic approach to solve timed games. Our solution gives a general framework to solve many classes of timed games via a translation to tree automata, extending to timed games a successful approach to solve discrete games. Our approach relies on translating a timed automaton into a tree automaton that accepts all the trees corresponding to a given strategy of the protagonist. This construction exploits the region automaton introduced by Alur and Dill. We use our framework to solve timed Buchi games in exponential time, timed Rabin games in exponential time, CTL games in exponential time and Ltl games in doubly exponential time. All these results are tight in the sense that they match the known lower bounds on these decision problems.