One-Counter Stochastic Games

We study the computational complexity of basic decision problems for one-counter simple stochastic games (OC-SSGs), under various objectives. OC-SSGs are 2-player turn-based stochastic games played on the transition graph of classic one-counter automata. We study primarily the termination objective, where the goal of one player is to maximize the probability of reaching counter value 0, while the other player wishes to avoid this. Partly motivated by the goal of understanding termination objectives, we also study certain "limit" and "long run average" reward objectives that are closely related to some well-studied objectives for stochastic games with rewards. Examples of problems we address include: does player 1 have a strategy to ensure that the counter eventually hits 0, i.e., terminates, almost surely, regardless of what player 2 does? Or that the lim inf (or lim sup) counter value equals with a desired probability? Or that the long run average reward is > ...

• Type: Journal
• Year: 2010
• Where: FSTTCS
• Authors: Tomás Brázdil, Václav Brozek, Kousha Etessami
• Keywords: FSTTCS 2010, Problems, Qualitative Termination Problems, Software Engineering, Stochastic Games