Citation
Krishnendu Chatterjee. "Stochastic Omega-Regular Games". PhD thesis, EECS Department, University of California, Berkeley, October, 2007.

Abstract
We study games played on graphs with omega-regular conditions specified as parity, Rabin, Streett or Muller conditions. These games have applications in the verification, synthesis, modeling, testing, and compatibility checking of reactive systems. Important distinctions between graph games are as follows: (a) turn-based vs. concurrent games, depending on whether at a state of the game only a single player makes a move, or players make moves simultaneously; (b) deterministic vs. stochastic, depending on whether the transition function is a deterministic or a probabilistic function over successor states; and (c) zero-sum vs. non-zero-sum, depending on whether the objectives of the players are strictly conflicting or not. We establish that the decision problem for turn-based stochastic zero-sum games with Rabin, Streett, and Muller objectives are NP-complete, coNP-complete, and PSPACE-complete, respectively, substantially improving the previously known 3EXPTIME bound. We also present strategy improvement style algorithms for turn-based stochastic Rabin and Streett games. In the case of concurrent stochastic zero-sum games with parity objectives we obtain a PSPACE bound, again improving the previously known 3EXPTIME bound. As a consequence, concurrent stochastic zero-sum games with Rabin, Streett, and Muller objectives can be solved in EXPSPACE, improving the previously known 4EXPTIME bound. We also present an elementary and combinatorial proof of the existence of memoryless epsilon-optimal strategies in concurrent stochastic games with reachability objectives, for all real epsilon>0, where an epsilon-optimal strategy achieves the value of the game with in epsilon against all strategies of the opponent. We also use the proof techniques to present a strategy improvement style algorithm for concurrent stochastic reachability games. We then go beyond omega-regular objectives and study the complexity of an important class of quantitative objectives, namely, limit-average objectives. In the case of limit-average games, the states of the graph is labeled with rewards and the goal is to maximize the long-run average of the rewards. We show that concurrent stochastic zero-sum games with limit-average objectives can be solved in EXPTIME. Finally, we introduce a new notion of equilibrium, called secure equilibrium, in non-zero-sum games which captures the notion of conditional competitiveness. We prove the existence of unique maximal secure equilibrium payoff profiles in turn-based deterministic games, and present algorithms to compute such payoff profiles. We also show how the notion of secure equilibrium extends the assume-guarantee style of reasoning in the game theoretic framework.

Electronic downloads

• http://www.eecs.berkeley.edu/Pubs/TechRpts/2007/EECS-2007-122.html

• HTML

  Krishnendu Chatterjee. <a
  href="http://chess.eecs.berkeley.edu/pubs/462.html"
  ><i>Stochastic Omega-Regular
  Games</i></a>, PhD thesis,  EECS Department,
  University of California, Berkeley, October, 2007.

• Plain text

  Krishnendu Chatterjee. "Stochastic Omega-Regular
  Games". PhD thesis,  EECS Department, University of
  California, Berkeley, October, 2007.

• BibTeX

  @phdthesis{Chatterjee07_StochasticOmegaRegularGames,
      author = {Krishnendu Chatterjee},
      title = {Stochastic Omega-Regular Games},
      school = {EECS Department, University of California, Berkeley},
      month = {October},
      year = {2007},
      abstract = {We study games played on graphs with omega-regular
                conditions specified as parity, Rabin, Streett or
                Muller conditions. These games have applications
                in the verification, synthesis, modeling, testing,
                and compatibility checking of reactive systems.
                Important distinctions between graph games are as
                follows: (a) turn-based vs. concurrent games,
                depending on whether at a state of the game only a
                single player makes a move, or players make moves
                simultaneously; (b) deterministic vs. stochastic,
                depending on whether the transition function is a
                deterministic or a probabilistic function over
                successor states; and (c) zero-sum vs.
                non-zero-sum, depending on whether the objectives
                of the players are strictly conflicting or not. We
                establish that the decision problem for turn-based
                stochastic zero-sum games with Rabin, Streett, and
                Muller objectives are NP-complete, coNP-complete,
                and PSPACE-complete, respectively, substantially
                improving the previously known 3EXPTIME bound. We
                also present strategy improvement style algorithms
                for turn-based stochastic Rabin and Streett games.
                In the case of concurrent stochastic zero-sum
                games with parity objectives we obtain a PSPACE
                bound, again improving the previously known
                3EXPTIME bound. As a consequence, concurrent
                stochastic zero-sum games with Rabin, Streett, and
                Muller objectives can be solved in EXPSPACE,
                improving the previously known 4EXPTIME bound. We
                also present an elementary and combinatorial proof
                of the existence of memoryless epsilon-optimal
                strategies in concurrent stochastic games with
                reachability objectives, for all real epsilon>0,
                where an epsilon-optimal strategy achieves the
                value of the game with in epsilon against all
                strategies of the opponent. We also use the proof
                techniques to present a strategy improvement style
                algorithm for concurrent stochastic reachability
                games. We then go beyond omega-regular objectives
                and study the complexity of an important class of
                quantitative objectives, namely, limit-average
                objectives. In the case of limit-average games,
                the states of the graph is labeled with rewards
                and the goal is to maximize the long-run average
                of the rewards. We show that concurrent stochastic
                zero-sum games with limit-average objectives can
                be solved in EXPTIME. Finally, we introduce a new
                notion of equilibrium, called secure equilibrium,
                in non-zero-sum games which captures the notion of
                conditional competitiveness. We prove the
                existence of unique maximal secure equilibrium
                payoff profiles in turn-based deterministic games,
                and present algorithms to compute such payoff
                profiles. We also show how the notion of secure
                equilibrium extends the assume-guarantee style of
                reasoning in the game theoretic framework.},
      URL = {http://chess.eecs.berkeley.edu/pubs/462.html}
  }
  

Posted by Christopher Brooks on 24 Jun 2008.
For additional information, see the Publications FAQ or contact webmaster at chess eecs berkeley edu.