Strategy Improvement for Concurrent Safety Games

We consider concurrent games played on graphs. At every round of the 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: "stay forever in a set F of states", and its dual, the reachability objective, "reach a set R of states". We present in this paper a strategy improvement algorithm for computing the value of a concurrent safety game, that is, the maximal probability with which player 1 can enforce the safety objective. The algorithm yields a sequence of player-1 strategies which ensure probabilities of winning that converge monotonically to the value of the safety game. The significance of the result is twofold. First, while strategy improvement algorithms were known for Markov decision processes and turn-based games, as well as for concurrent reachability games, this is the first strategy improvement algorithm for concurrent safety games...

• Type: Journal
• Year: 2008
• Where: CORR
• Authors: Krishnendu Chatterjee, Luca de Alfaro, Thomas A. Henzinger
• Keywords: Algorithm, Concurrent Safety Game, CORR 2008, Education, Safety Games