TY - JOUR AU - Walukiewicz, Igor PY - 1996/06/24 Y2 - 2024/03/28 TI - Pushdown Processes: Games and Model Checking JF - BRICS Report Series JA - BRICS VL - 3 IS - 54 SE - Articles DO - 10.7146/brics.v3i54.20057 UR - https://tidsskrift.dk/brics/article/view/20057 SP - AB - Games given by transition graphs of pushdown processes are considered.<br />It is shown that if there is a winning strategy in such a<br />game then there is a winning strategy that is realized by a pushdown<br />process. This fact turns out to be connected with the model checking<br />problem for the pushdown automata and the propositional mu-calculus.<br />It is shown that this model checking problem is DEXPTIME-complete. ER -