A pushdown system is a graph $G(P)$ of configurations of a
pushdown automaton $P$. The model checking problem} for a logic
$L$ is: given a pushdown automaton $P$ and a formula $\a\in L$ decide
if $\a$ holds in the vertex of $G(P)$ which is the initial
configuration of $P$. Computation Tree Logic (CTL) and its fragment EF
are considered. The model checking problems for CTL and EF are shown
to be EXPTIME-complete and PSPACE-complete, respectively.
