In *Proceedings of the 9th International Conference on Foundations of Software Science and Computational Structures (FoSSaCS 2006)*, volume 3921, of *Lecture Notes in Computer Science*, pages 337-351, 2006. Springer-Verlag.

abstract bibtex

abstract bibtex

We consider parity games played on special pushdown graphs, namely those generated by one-counter processes. For parity games on pushdown graphs, it is known from [Wal96] that deciding the winner is an Exptime-complete problem. An important corollary of this result is that the mu-calculus model checking problem for pushdown processes is Exptime-complete. As one-counter processes are special cases of pushdown processes, it follows that deciding the winner in a parity game played on the transition graph of a one-counter process can be achieved in Exptime. Nevertheless the proof for the Exptime-hardness lower bound of [Wal] cannot be adapted to that case. Therefore, a natural question is whether the Exptime upper bound can be improved in this special case. In this paper, we adapt techniques from [KV00,Cac02c] and provide a Pspace upper bound and a DP-hard lower bound for this problem. We also give two important consequences of this result. First, we improve the best upper bound known for model-checking one-counter processes against mu-calculus. Second, we show how these games can be used to solve pushdown games with winning conditions that are Boolean combinations of a parity condition on the control states with conditions on the stack height.

@inproceedings{TTSerre06, keywords={perso,conf,ERC}, author = {Olivier Serre}, title = {Parity Games Played on Transition Graphs of One-Counter Processes}, Booktitle = {Proceedings of the 9th International Conference on Foundations of Software Science and Computational Structures (FoSSaCS 2006)}, year = {2006}, pages = {337-351}, volume = {3921}, Publisher = "Springer-Verlag", Series = "Lecture Notes in Computer Science", abstract = {We consider parity games played on special pushdown graphs, namely those generated by one-counter processes. For parity games on pushdown graphs, it is known from [Wal96] that deciding the winner is an Exptime-complete problem. An important corollary of this result is that the mu-calculus model checking problem for pushdown processes is Exptime-complete. As one-counter processes are special cases of pushdown processes, it follows that deciding the winner in a parity game played on the transition graph of a one-counter process can be achieved in Exptime. Nevertheless the proof for the Exptime-hardness lower bound of [Wal] cannot be adapted to that case. Therefore, a natural question is whether the Exptime upper bound can be improved in this special case. In this paper, we adapt techniques from [KV00,Cac02c] and provide a Pspace upper bound and a DP-hard lower bound for this problem. We also give two important consequences of this result. First, we improve the best upper bound known for model-checking one-counter processes against mu-calculus. Second, we show how these games can be used to solve pushdown games with winning conditions that are Boolean combinations of a parity condition on the control states with conditions on the stack height.}, fulltexturl = {http://hal.archives-ouvertes.fr/hal-00016665}, }

Downloads: 0