Abstract
Games given by transition graphs of pushdown processes are considered. It is shown that if there is a winning strategy in such a game then there is a winning strategy which is realized by a pushdown process. This fact turns out to be connected with the model checking problem for pushdown automata and the propositional µ-calculus. It is show that this model checking problem is DEXPTIME-complete.
Cite
CITATION STYLE
Walukiewicz, I. (1996). Pushdown processes: Games and model checking. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 1102, pp. 62–74). Springer Verlag. https://doi.org/10.1007/3-540-61474-5_58
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
