In this paper we study model checking of pushdown specifications. Our specification formalism is nondeterministic pushdown parity tree automata (PD-NPT). We show that the model-checking problem for regular systems and PD-NPT specifications can be solved in time exponential in the system and the specification. Our model-checking algorithm involves a new solution to the nonemptiness problem of nondeterministic pushdown tree automata, where we improve the best known upper bound from a triple-exponential to a single exponential. We also consider the model-checking problem for context-free systems and PD-NPT specifications and show that it is undecidable.
@inproceedings{KPV02a,
author = "O. Kupferman and N. Piterman and M. Vardi",
title = "Pushdown Specifications",
booktitle = "9th International Conference on Logic for Programming Artificial Intelligence and Reasoning",
series = "Lecture Notes in Artificial Inteligence",
month = "October",
year = 2002
}