We consider turn-based stochastic two-player games with a combination of a parity condition that must hold surely, that is in all possible outcomes, and of a parity condition that must hold almost-surely, that is with probability 1. The problem of deciding the existence of a winning strategy in such games is central in the framework of synthesis beyond worst-case where a hard requirement that must hold surely is combined with a softer requirement. Recent works showed that the problem is coNP-complete, and infinite-memory strategies are necessary in general, even in one-player games (i.e., Markov decision processes). However, memoryless strategies are sufficient for the opponent player. Despite these comprehensive results, the known algorithmic solution enumerates all memoryless strategies of the opponent, which is exponential in all cases, and does not construct a winning strategy when one exists. We present a recursive algorithm, based on a characterisation of the winning region, that gives a deeper insight into the problem. In particular, we show how to construct a winning strategy to achieve the combination of sure and almost-sure parity, and we derive new complexity and memory bounds for special classes of the problem, defined by fixing the index of either of the two parity conditions.

翻译：我们研究回合制随机双人博弈，其中结合了一个必须确定满足（即在所有可能结果中均成立）的奇偶条件，以及一个必须几乎确定满足（即以概率1成立）的奇偶条件。在此类博弈中判定获胜策略存在性的问题，是超越最坏情况综合框架的核心问题，该框架将必须确定满足的硬性要求与较宽松的要求相结合。近期研究表明该问题是coNP完全的，且通常需要无限记忆策略（即使在单人博弈中，即马尔可夫决策过程）。然而，对手玩家仅需无记忆策略即可。尽管已有这些全面结论，现有算法方案仍需枚举对手的所有无记忆策略，这在所有情况下均具有指数复杂度，且无法在存在获胜策略时构建具体策略。我们提出一种基于获胜区域表征的递归算法，为该问题提供更深入的见解。特别地，我们展示了如何构建获胜策略以实现确定性与几乎确定性奇偶条件的结合，并针对通过固定两个奇偶条件中任一指标定义的特殊问题类别，推导出新的复杂度界限与内存需求界限。