The rapid development of complex and
safety-critical systems requires the use of
reliable verification methods and tools for system design (synthesis).
Many systems of interest are reactive, in the sense that
their behavior depends on the interaction with the environment.
A natural framework to model them is a two-player
game: the system versus the environment.
In this context, the central problem is to determine the existence
of a winning strategy according to a given
winning condition.
We focus on real-time systems, and choose to model the related game
as a nondeterministic timed automaton.
We express winning conditions by formulas in
the universal fragment of the branching-time logic \tctl\ ($\forall$\tctl).
The main result of this paper is an exponential-time algorithm to
check for the existence of a winning strategy for $\forall$\tctl\ games
where the equality is not allowed in the timing constraints.
This result matches the known lower bound on timed games.
Moreover, if we relax the limitation we have placed on the timing
constraints, the problem becomes undecidable.
