TY - GEN
T1 - Parity games played on transition graphs of one-counter processes
AU - Serre, Olivier
PY - 2006/7/14
Y1 - 2006/7/14
N2 - 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 [23] that deciding the winner is an ExpTIME-complete problem. An important corollary of this result is that the μ-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 [23] 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 [11, 4] 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 μ-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.
AB - 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 [23] that deciding the winner is an ExpTIME-complete problem. An important corollary of this result is that the μ-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 [23] 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 [11, 4] 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 μ-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.
U2 - 10.1007/11690634_23
DO - 10.1007/11690634_23
M3 - Conference contribution
AN - SCOPUS:33745790034
SN - 3540330453
SN - 9783540330455
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 337
EP - 351
BT - Foundations of Software Science and Computation Structures - 9th International Conf., FOSSACS 2006. Held as Part of the Joint European Conf. on Theory and Practice of Software, ETAPS 2006, Proc.
T2 - 9th International Conference on Foundations of Software Science and Computation Structures, FOSSACS 2006. Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2006
Y2 - 25 March 2006 through 31 March 2006
ER -