Skip to main content

1996 | ReviewPaper | Buchkapitel

Pushdown processes: Games and model checking

Extended abstract

verfasst von : Igor Walukiewicz

Erschienen in: Computer Aided Verification

Verlag: Springer Berlin Heidelberg

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config
loading …

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 push-down automata and the propositional μ-calculus. It is show that this model checking problem is DEXPTIME-complete.

Metadaten
Titel
Pushdown processes: Games and model checking
verfasst von
Igor Walukiewicz
Copyright-Jahr
1996
Verlag
Springer Berlin Heidelberg
DOI
https://doi.org/10.1007/3-540-61474-5_58