Reachability Analysis of Pushdown Automata: Application to Model-Checking

We apply the symbolic analysis principle to pushdown systems. We represent (possibly in nite) sets of con gurations of such systems by means of nite-state automata. In order to reason in a uniform way about analysis problems involving both existential and universal path quanti cation (like model-checking for branching-time logics), we consider the more general class of alternating pushdown systems and use alternating nite-state automata as a representation structure for their sets of con gurations. 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 de ne 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.

• Type: Conference
• Year: 1997
• Where: CONCUR
• Authors: Ahmed Bouajjani, Javier Esparza, Oded Maler
• Keywords: CONCUR 1997, Distributed And Parallel Computing, Nite-state Automata, Pushdown Systems, Representation Structure