With such shared/common knowledge problems, even when AC isn't involved, I think a crucial first step is to get away from the "story" version. For example, since this is only interesting once the set of murderers is uncountable (since it needs to be non-wellorderable), talking about probabilities isn't going to be ultimately helpful.

Here's a first stab at a formalization:

Consider, for $X$ a set, a two-player game $\mathsf{Shoot}_X$ played as follows:

• First, player $1$ plays a function $f:\mathcal{P}(X)\rightarrow\mathcal{P}(X)$ satisfying $f(S)\subseteq S$ for all $S\subseteq X$.

• Next, player $2$ plays a function $g: X\rightarrow 2$.

• At this point, the game is done: player $2$ wins iff $f(g^{-1}(1))$ has more than one element.

The intuition here is that player $1$ is announcing their shooting strategy ("If the set of runners is $S$, I'll 'randomly' shoot someone in $f(S)$") and player $2$ is saying which murderers (= elements of $X$) will run. The condition that $f(g^{-1}(1))$ has more than one element corresponds to every runner having a chance of surviving.

This formalization more-or-less trivializes things: a winning strategy for player $1$ must be a choice function for $\mathcal{P}_{\not=\emptyset}(X)$, and so the existence of a winning strategy for player $1$ for all $X$ is automatically equivalent to choice. I think this highlights the importance of making the infinitary version of the game more precise.

This does, however, raise an interesting follow-up question:

Is $\mathsf{ZF}$ + $\neg\mathsf{AC}$ + "Every $\mathsf{Shoot}_X$-game is determined" consistent?

I suspect there's an easy argument that the answer is negative (= that from a failure of choice we can build an undetermined shooting game), but I don't immediately see it.

With such shared/common knowledge problems, even when AC isn't involved, I think a crucial first step is to get away from the "story" version. For example, since this is only interesting once the set of murderers is uncountable (since it needs to be non-wellorderable), talking about probabilities isn't going to be ultimately helpful.

Here's a first stab at a formalization:

Consider, for $X$ a set, a two-player game $\mathsf{Shoot}_X$ played as follows:

• First, player $1$ plays a function $f:\mathcal{P}(X)\rightarrow\mathcal{P}(X)$ satisfying $f(S)\subseteq S$ for all $S\subseteq X$.

• Next, player $2$ plays a function $g: X\rightarrow 2$.

• At this point, the game is done: player $2$ wins iff $f(g^{-1}(1))$ has more than one element.

The intuition here is that player $1$ is announcing their shooting strategy ("If the set of runners is $S$, I'll 'randomly' shoot someone in $f(S)$") and player $2$ is saying which murderers (= elements of $X$) will run. The condition that $f(g^{-1}(1))$ has more than one element corresponds to every runner having a chance of surviving.

This formalization more-or-less trivializes things (since the game itself is basically $\mathsf{AC}$ in disguise): a winning strategy for player $1$ must be a choice function for $\mathcal{P}_{\not=\emptyset}(X)$, and so the existence of a winning strategy for player $1$ for all $X$ is automatically equivalent to choice. In fact, I think this highlights the importance of making the infinitary version of the game more precise.

This does, however, raise an interesting follow-up question:

Is $\mathsf{ZF}$ + $\neg\mathsf{AC}$ + "Every $\mathsf{Shoot}_X$-game is determined" consistent?

I suspect there's an easy argument that the answer is negative (= that from a failure of choice we can build an undetermined shooting game), but I don't immediately see it.