  Timed pushdown automata (TPDA) are an expressive formalism combining
recursion with a rich logic of timing constraints. We prove that reachability
relations of TPDA are expressible in linear arithmetic, a rich logic
generalising Presburger arithmetic and rational arithmetic. The main technical
ingredients are a novel quantifier elimination result for clock constraints
(used to simplify the syntax of TPDA transitions), the use of clock difference
relations to express reachability relations of the fractional clock values, and
an application of Parikh's theorem to reconstruct the integral clock values.
