@article{2854,
  abstract     = {We consider concurrent games played on graphs. At every round of a game, each player simultaneously and independently selects a move; the moves jointly determine the transition to a successor state. Two basic objectives are the safety objective to stay forever in a given set of states, and its dual, the reachability objective to reach a given set of states. First, we present a simple proof of the fact that in concurrent reachability games, for all ε>0, memoryless ε-optimal strategies exist. A memoryless strategy is independent of the history of plays, and an ε-optimal strategy achieves the objective with probability within ε of the value of the game. In contrast to previous proofs of this fact, our proof is more elementary and more combinatorial. Second, we present a strategy-improvement (a.k.a. policy-iteration) algorithm for concurrent games with reachability objectives. Finally, we present a strategy-improvement algorithm for turn-based stochastic games (where each player selects moves in turns) with safety objectives. Our algorithms yield sequences of player-1 strategies which ensure probabilities of winning that converge monotonically (from below) to the value of the game. © 2012 Elsevier Inc.},
  author       = {Chatterjee, Krishnendu and De Alfaro, Luca and Henzinger, Thomas A},
  journal      = {Journal of Computer and System Sciences},
  number       = {5},
  pages        = {640 -- 657},
  publisher    = {Elsevier},
  title        = {{Strategy improvement for concurrent reachability and turn based stochastic safety games}},
  doi          = {10.1016/j.jcss.2012.12.001},
  volume       = {79},
  year         = {2013},
}