## Termination Criteria for Solving Concurrent Safety and Reachability
Games

*Krishnendu Chatterjee, Luca de Alfaro, and
Thomas A. Henzinger*

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. 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.

Our result is significant because the strategy improvement algorithm
provides, for the first time, a way to approximate the value of a
concurrent safety game *from below*. Since a value iteration
algorithm, or a strategy improvement algorithm for reachability games,
can be used to approximate the same value from above, the combination
of both algorithms yields a method for computing a converging sequence
of upper and lower bounds for the values of concurrent reachability
and safety games. Previous methods could approximate the values of
these games only from one direction, and as no rates of convergence
are known, they did not provide a practical way to solve these games.

*Proceedings of the
20th Annual Symposium on Discrete Algorithms*
(SODA),
ACM Press,
2009.

Download inofficial, sometimes updated
PostScript /
PDF document.
© 2009 ACM.