We investigate zero-sum turn-based two-player stochastic games in which the objective of one player is to maximize the amount of rewards obtained during a play, while the other aims at minimizing it. We focus on games in which the minimizer plays in a fair way. We believe that these kinds of games enjoy interesting applications in software verification, where the maximizer plays the role of a system intending to maximize the number of "milestones" achieved, and the minimizer represents the behavior of some uncooperative but yet fair environment. Normally, to study total reward properties, games are requested to be stopping (i.e., they reach a terminal state with probability 1). We relax the property to request that the game is stopping only under a fair minimizing player. We prove that these games are determined, i.e., each state of the game has a value defined. Furthermore, we show that both players have memoryless and deterministic optimal strategies, and the game value can be computed by approximating the greatest-fixed point of a set of functional equations. We implemented our approach in a prototype tool, and evaluated it on an illustrating example and an Unmanned Aerial Vehicle case study.
翻译:我们调查了以零和回合为基础的双玩家随机游戏,其中,一个玩家的目标是最大限度地增加游戏期间获得的奖赏,而另一个目的是最大限度地减少这种奖赏。我们侧重于最小化者以公平的方式玩耍的游戏。我们相信,这些游戏在软件核查中享有有趣的应用,在软件核查中,最大化者扮演着一个旨在最大限度地增加所达到的“里程碑”数量的系统的作用,而最小化者则代表着一些不合作但公平的环境的行为。通常,为了研究总奖赏属性,游戏被要求停止(即,他们达到极点,概率为1 ) 。我们放松了财产,要求游戏只停止在一个公平的最小化玩家手中。我们证明这些游戏是确定的,即每个游戏的状态都有一定的价值。此外,我们证明两个玩家都有没有记忆和确定性的最佳策略,游戏的价值可以通过接近一套最精细的功能方程来计算。我们用原型工具实施了我们的方法,并在一个显示车辆示例和不正规的案例研究上评估了它。