Optimal Strategies in Infinite-state Stochastic Reachability Games

TL;DR

This paper studies a specific class of infinite-state stochastic reachability games, proving that Player Max always has optimal strategies and that these games are strongly determined, with implications for One-Counter stochastic games.

Contribution

It identifies a subclass of infinite-state stochastic games where Player Max has optimal strategies and proves strong determinacy, extending recent finite-branching game results.

Findings

Player Max always has optimal strategies in the subclass.

The subclass of games is strongly determined.

Results apply to One-Counter stochastic games.

Abstract

We consider perfect-information reachability stochastic games for 2 players on infinite graphs. We identify a subclass of such games, and prove two interesting properties of it: first, Player Max always has optimal strategies in games from this subclass, and second, these games are strongly determined. The subclass is defined by the property that the set of all values can only have one accumulation point -- 0. Our results nicely mirror recent results for finitely-branching games, where, on the contrary, Player Min always has optimal strategies. However, our proof methods are substantially different, because the roles of the players are not symmetric. We also do not restrict the branching of the games. Finally, we apply our results in the context of recently studied One-Counter stochastic games.