@inproceedings{481ccd76f705443abe170770bcd4b104,
title = "Reachability analysis of pushdown automata: Application to model-checking",
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 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 {\textquoteleft}pushdown{\textquoteright} 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.",
author = "Ahmed Bouajjani and Javier Esparza and Oded Maler",
note = "Publisher Copyright: {\textcopyright} Springer-Verlag Berlin Heidelberg 1997.; 8th International Conference on Concurrency Theory, CONCUR 1997 ; Conference date: 01-07-1997 Through 04-07-1997",
year = "1997",
doi = "10.1007/3-540-63141-0_10",
language = "English",
isbn = "3540631410",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "135--150",
editor = "Antoni Mazurkiewicz and J{\'o}zef Winkowski",
booktitle = "CONCUR 1997",
}