Banach-Mazur Parity Games and Almost-sure Winning Strategies

Two-player stochastic games are games with two 2 players and a randomised entity called "nature". A natural question to ask in this framework is the existence of strategies that ensure that an event happens with probability 1 (almost-sure strategies). In the case of Markov decision processes, when the event 2 of interest is given as a parity condition, we can replace the "nature" by two more players that play according to the rules of what is known as Banach-Mazur game [1]. In this paper we continue this research program by extending the above result to two-player stochastic parity games. As in the paper [1], the basic idea is that, under the correct hypothesis, we can replace the randomised player with two players playing a Banach-Mazur game. This requires a few technical observations, and a non trivial proof, that this paper sets out to do.