This paper gives a simple and direct algorithm for computing the always regular set of reachable states of a pushdown system. It then exploits this algorithm for obtaining model checking algorithms for linear-time temporal logic as well as for the logic CTL∗. For the latter, a new technical tool is introduced: pushdown automata with transitions conditioned on regular predicates on the stack content. Finally, this technical tool is also used to establish that CTL∗ model checking remains decidable when the formulas are allowed to include regular predicates on the stack content.
