*banner
 

Stochastic Omega-Regular Games
Krishnendu Chatterjee

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

Citation formats  
  • 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.

Notice: This material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All persons copying this information are expected to adhere to the terms and constraints invoked by each author's copyright.

©2002-2018 Chess