I7 Logo
Chair for Foundations of Software Reliability and Theoretical Computer Science
Informatik Logo TUM Logo
Publications - Reachability Analysis of Pushdown Automata: Application to Model-Checking


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


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:

    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}

GZipped PostScript (154 kB)
PDF (430 kB)