View article

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.