Parity Games Played on Transition Graphs of One-Counter Processes. Serre, O. 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   
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