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 a uniform way about analysis problems involving both existential and universal path quantification (such as 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 sets of their configurations. We give a simple and natural procedure to compute sets of predecessors using this representation structure. We incorporate this procedure into the automata-theoretic approach to model-checking to define new model-checking algorithms for pushdown systems against both linear and branching-time properties. Prom these results we derive upper bounds for several model-checking problems as well as matching lower bounds.
CITATION STYLE
Bouajjani, A., Esparza, J., & Maler, O. (1997). Reachability analysis of pushdown automata: Application to model-checking. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 1243, pp. 135–150). Springer Verlag. https://doi.org/10.1007/3-540-63141-0_10
Mendeley helps you to discover research relevant for your work.