Pushdown Processes: Games and Model Checking

Authors

  • Igor Walukiewicz

DOI:

https://doi.org/10.7146/brics.v3i54.20057

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 that is realized by a pushdown
process. This fact turns out to be connected with the model checking
problem for the pushdown automata and the propositional mu-calculus.
It is shown that this model checking problem is DEXPTIME-complete.

Downloads

Published

1996-06-24

How to Cite

Walukiewicz, I. (1996). Pushdown Processes: Games and Model Checking. BRICS Report Series, 3(54). https://doi.org/10.7146/brics.v3i54.20057