We consider turn-based stochastic games on infinite graphs induced by game probabilistic lossy channel systems (GPLCS), the game version of probabilistic lossy channel systems (PLCS). We study games with Buchi (repeated reachability) objectives and almost-sure winning condition. Under the assumption that the target set is regular, a symbolic representation of the set of winning states for each player can be effectively constructed. Thus, turn-based stochastic games on GPLCS are decidable. This generalizes earlier decidability result for PLCS-induced Markov decision processes. Our scheme can be adapted to GPLCS with simple reachability objectives.
Note: Updated 14 December 2007. To appear in the proceedings of FoSSaCS 2008.
Available as PDF (245 kB), compressed Postscript (185 kB), Postscript (1.01 MB, no cover), compressed Postscript (512 kB), PDF (274 kB), compressed Postscript (512 kB, no cover), Postscript (426 kB), PDF (274 kB, no cover), Postscript (1 MB), compressed Postscript (212 kB), and PDF (509 kB)
Download BibTeX entry.