One-counter processes (OCPs) are pushdown processes which operate only on a
unary stack alphabet. We study the computational complexity of model checking
computation tree logic (CTL) over OCPs. A PSPACE upper bound is inherited from
the modal mu-calculus for this problem. First, we analyze the periodic
behaviour of CTL over OCPs and derive a model checking algorithm whose running
time is exponential only in the number of control locations and a syntactic
notion of the formula that we call leftward until depth.