Optimal Strategies in Concurrent Reachability Games

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 𝖡, 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 ε > 0, Player 𝖠 has a strategy that maximizes up to ε the probability to win. Our work is two-fold. First, we present a double-fixed-point procedure that says from which state Player 𝖠 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 ε > 0, Player 𝖠 has a positional strategy that maximizes the probability to win, exactly from maximizable states and up to ε 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 𝖠 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 𝖠 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.