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) ⊆ 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.
This research was supported in part by the grants NSF CCR-0427202 and NSF CNS-0541606.