Optimal strategies in concurrent reachability games

TL;DR

This paper develops a method to determine optimal strategies in concurrent reachability games, providing a fixed-point procedure for exact probability maximization and characterizing conditions for positional strategies in small and larger games.

Contribution

Introduces a double-fixed-point procedure for exact probability maximization and characterizes local interactions guaranteeing positional optimal strategies.

Findings

A fixed-point method computes states where Player A can maximize winning probability.

Positional strategies exist for maximizable states and approximate maximization in others.

Certain local interactions in small and large games ensure the existence of uniform optimal strategies.

Abstract

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.