  A recent result of Haase et al. has shown that reachability in two-clock
timed automata is log-space equivalent to reachability in bounded one-counter
automata. We show that reachability in bounded one-counter automata is
PSPACE-complete.
