Reachability Analysis of Pushdown Automata: Application to Model-Checking

摘要: We apply the symbolic analysis principle to pushdown systems. represent (possibly infinite) sets of configurations such systems by means finite-state automata. In order reason in a uniform way about problems involving both existential and universal path quantification (such as model-checking for branching-time logics), we consider more general class alternating use automata representation structure their configurations. give simple natural procedure compute predecessors using this structure. incorporate into automata-theoretic approach define new algorithms against linear properties. From these results derive upper bounds several well matching lower bounds.