We study two questions in the theory of timed automata
concerning timed language inclusion of real-time programs modeled as timed
pushdown automata in real-time specifications with just one clock. We show that
if the specification B is modeled as a timed automaton with one clock,
then the language inclusion problem L(A)\subseteq
L(B) for a timed pushdown automaton A is decidable. On the
other hand, we show that the universality problem of timed visibly pushdown
automata with only one clock is undecidable. Thus there is no algorithm to
check language inclusion of real-time programs for specifications given by
visibly pushdown specifications with just one clock.