Sciweavers

Share
CONCUR
1997
Springer

Reachability Analysis of Pushdown Automata: Application to Model-Checking

9 years 2 months ago
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.
Ahmed Bouajjani, Javier Esparza, Oded Maler
Added 07 Aug 2010
Updated 07 Aug 2010
Type Conference
Year 1997
Where CONCUR
Authors Ahmed Bouajjani, Javier Esparza, Oded Maler
Comments (0)
books