  The focus of this paper is the analysis of real-time systems with recursion,
through the development of good theoretical techniques which are implementable.
Time is modeled using clock variables, and recursion using stacks. Our
technique consists of modeling the behaviours of the timed system as graphs,
and interpreting these graphs on tree terms by showing a bound on their
tree-width. We then build a tree automaton that accepts exactly those tree
terms that describe realizable runs of the timed system. The emptiness of the
timed system thus boils down to emptiness of a finite tree automaton that
accepts these tree terms. This approach helps us in obtaining an optimal
complexity, not just in theory (as done in earlier work), but also in going
towards an efficient implementation of our technique. To do this, we make
several improvements in the theory and exploit these to build a first prototype
tool that can analyze timed systems with recursion.
