Some new papers uploaded to ArXiv on Stochastic games

There are a few uploads of papers on stochastic games in ArXiv recently. The common author in all of them is Krishnendu Chatterjee.

1. Magnifying Lens Abstraction for Stochastic Games with Discounted and Long-run Average Objectives

Authors: Krishnendu Chatterjee and Luca de Alfaro and Pritam Roy

Turn-based stochastic games and its important subclass Markov decision processes (MDPs) provide models for systems with both probabilistic and nondeterministic behaviors. We consider turn-based stochastic games with two classical quantitative objectives: discounted-sum and long-run average objectives. The game models and the quantitative objectives are widely used in probabilistic verification, planning, optimal inventory control, network protocol and performance analysis. Games and MDPs that model realistic systems often have very large state spaces, and probabilistic abstraction techniques are necessary to handle the state-space explosion. The commonly used full-abstraction techniques do not yield space-savings for systems that have many states with similar value, but does not necessarily have similar transition structure. A semi-abstraction technique, namely Magnifying-lens abstractions (MLA), that clusters states based on value only, disregarding differences in their transition relation was proposed for qualitative objectives (reachability and safety objectives). In this paper we extend the MLA technique to solve stochastic games with discounted-sum and long-run average objectives. We present the MLA technique based abstraction-refinement algorithm for stochastic games and MDPs with discounted-sum objectives. For long-run average objectives, our solution works for all MDPs and a sub-class of stochastic games where every state has the same value.

ArXiv Paper

2. Partial-Observation Stochastic Games: How to Win when Belief Fails

Authors: Krishnendu Chatterjee and Laurent Doyen

In two-player finite-state stochastic games of partial observation on graphs, in every state of the graph, the players simultaneously choose an action, and their joint actions determine a probability distribution over the successor states. We consider reachability objectives where player 1 tries to ensure a target state to be visited almost-surely or positively. On the basis of information, the game can be one-sided with either (a)player 1 or (b)player 2 having partial observation, or two-sided with both players having partial observation. On the basis of randomization (a)players may not be allowed to use randomization (pure strategies), or (b)may choose a probability distribution over actions but the actual random choice is not visible (actions invisible), or (c)may use full randomization. Our results for pure strategies are as follows: (1)For one-sided games with player 2 perfect observation we show that belief-based strategies are not sufficient, and present an exponential upper bound on memory both for almost-sure and positive winning strategies; we show that the problem of deciding the existence of almost-sure and positive winning strategies for player 1 is EXPTIME-complete and present symbolic algorithms that avoid the explicit exponential construction. (2)For one-sided games with player 1 perfect observation we show that non-elementary memory is both necessary and sufficient for both almost-sure and positive winning strategies. (3)We show that for the two-sided case finite memory strategies are sufficient for both positive and almost-sure winning. We establish the equivalence of the almost-sure winning problem for pure strategies with randomized strategies with actions invisible. Our equivalence result exhibit serious flaws in previous results in the literature: we show a non-elementary memory lower bound for almost-sure winning whereas an exponential upper bound was claimed.

ArXiv Paper

3. Bounded Rationality in Concurrent Parity Games

Authors: Krishnendu Chatterjee

We consider 2-player games played on a finite state space for infinite rounds. The games are concurrent: in each round, the two players choose their moves simultaneously; the current state and the moves determine the successor. We consider omega-regular winning conditions given as parity objectives. We consider the qualitative analysis problems: the computation of the almost-sure and limit-sure winning set of states, where player 1 can ensure to win with probability 1 and with probability arbitrarily close to 1, respectively. In general the almost-sure and limit-sure winning strategies require both infinite-memory and infinite-precision. We study the bounded-rationality problem for qualitative analysis of concurrent parity games, where the strategy set player 1 is restricted to bounded-resource strategies. In terms of precision, strategies can be deterministic, uniform, finite-precision or infinite-precision; and in terms of memory, strategies can be memoryless, finite-memory or infinite-memory. We present a precise and complete characterization of the qualitative winning sets for all combinations of classes of strategies. In particular, we show that uniform memoryless strategies are as powerful as finite-precision infinite-memory strategies, and infinite-precision memoryless strategies are as powerful as infinite-precision finite-memory strategies. We show that the winning sets can be computed in time, where n is the size of the game and 2d is the number of priorities, and our algorithms are symbolic. The membership problem of whether a state belongs to a winning set can be decided in NP cap coNP. While this complexity is the same as for the simpler class of turn-based games, where in each state only one of the players has a choice of moves, our algorithms, that are obtained by characterization of the winning sets as mu-calculus formulas, are considerably more involved.

ArXiv Paper