Reference:

A. Bouajjani, J. Esparza, and O. Maler. Reachability analysis of pushdown automata: Application to model-checking. In Proc. of CONCUR'97, 1997.

Abstract:

We apply the symbolic analysis principle to pushdown systems. We represent (possibly infinite) sets of configurations of such systems by means of finite-state automata. In order to reason in an uniform way about analysis problems involving both existential and universal path quantification (like model-checking for branching-time logics), we consider the more general class of alternating pushdown systems and use alternating finite-state automata as a representation structure for their sets of configurations. We give a simple and natural procedure to compute sets of predecessors for this representation structure. We apply this procedure and the automata-theoretic approach to model-checking to define new model-checking algorithms for pushdown systems and both linear and branching time properties. From these results we derive upper bounds for several model-checking problems, and we also provide matching lower bounds, using reductions based on some techniques introduced by Walukiewicz.

Suggested BibTeX entry:

@inproceedings{BEM97,
    author = {A. Bouajjani and J. Esparza and O. Maler},
    booktitle = {Proc. of CONCUR'97},
    title = {Reachability Analysis of Pushdown Automata: {A}pplication to Model-Checking},
    year = {1997}
}