We consider pushdown timed automata (PTAs) that are timed automata
(with dense clocks) augmented with a pushdown stack. A configuration
of a PTA includes a control state, dense clock values
and a stack word. By using the pattern technique,
we give a decidable characterization of
the binary reachability (i.e., the set of
all pairs of configurations such that
one can reach the other) of a PTA.
Since a timed automaton can be treated as
a PTA without the pushdown stack,
we can show that the binary reachability of a timed automaton
is definable in the additive theory of reals and integers.
The results can be used to verify a class
of properties containing linear relations
over both dense variables and unbounded discrete variables.
The properties previously could not be
verified using the classic region technique
nor expressed by timed temporal logics for timed automata
and CTL$^*$ for pushdown systems.
