K. Chatterjee,
L. de Alfaro,
T.A. Henzinger.
Termination Criteria for Solving Concurrent
Safety and Reachability Games.
In Proceedings of SODA 09: ACM-SIAM Symposium on Discrete
Algorithms, ACM Press, 2009.
Abstract
PDF
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.
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.