  We study two-player reachability games on finite graphs. At each state the
interaction between the players is concurrent and there is a stochastic Nature.
Players also play stochastically. The literature tells us that 1) Player B, who
wants to avoid the target state, has a positional strategy that maximizes the
probability to win (uniformly from every state) and 2) from every state, for
every {\epsilon} > 0, Player A has a strategy that maximizes up to {\epsilon}
the probability to win. Our work is two-fold. First, we present a
double-fixed-point procedure that says from which state Player A has a strategy
that maximizes (exactly) the probability to win. This is computable if Nature's
probability distributions are rational. We call these states maximizable.
Moreover, we show that for every {\epsilon} > 0, Player A has a positional
strategy that maximizes the probability to win, exactly from maximizable states
and up to {\epsilon} from sub-maximizable states. Second, we consider
three-state games with one main state, one target, and one bin. We characterize
the local interactions at the main state that guarantee the existence of an
optimal Player A strategy. In this case there is a positional one. It turns out
that in many-state games, these local interactions also guarantee the existence
of a uniform optimal Player A strategy. In a way, these games are well-behaved
by design of their elementary bricks, the local interactions. It is decidable
whether a local interaction has this desirable property.

Computer Science and Game Theory