Decision procedures for alternating timed automata

Alternating timed automata extend Alur-Dill timed automata to obtain closure under all Boolean operations. However, over dense infinite time domains (such as the reals) they have an undecidable language emptiness problem.

Our main result is that the restriction to bounded time restores decidability of the language emptiness problem. The proof of this involves solving a parametrized version of Church's synthesis problem over bounded real time. This problem is expressed as a McNaughton game played over timed words with a monadic winning condition.