title: Strategy improvement for concurrent reachability and turn-based stochastic safety games.
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 [Formula: see text], 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.
authors.affiliation: IST Austria (Institute of Science and Technology Austria), Austria.
authors.forename: Krishnendu
authors.initials: K
authors.lastname: Chatterjee
authors.affiliation: University of California, Santa Cruz, United States.
authors.forename: Luca
authors.initials: L
authors.lastname: de Alfaro
authors.affiliation: IST Austria (Institute of Science and Technology Austria), Austria.
authors.forename: Thomas A
authors.initials: TA
authors.lastname: Henzinger
keywords: Concurrent games; Game theory; Reachability and safety objectives; Stochastic games; Strategy-improvement algorithms