We compare games under delayed control and delay games, two types of infinite games modelling asynchronicity in reactive synthesis. In games under delayed control both players suffer from partial informedness due to symmetrically delayed communication, while in delay games, the protagonist has to grant lookahead to the alter player. Our first main result, the interreducibility of the existence of sure winning strategies for the protagonist, allows to transfer known complexity results and bounds on the delay from delay games to games under delayed control, for which no such results had been known. We furthermore analyse existence of randomized strategies that win almost surely, where this correspondence between the two types of games breaks down. In this setting, some games surely won by the alter player in delay games can now be won almost surely by the protagonist in the corresponding game under delayed control, showing that it indeed makes a difference whether the protagonist has to grant lookahead or both players suffer from partial informedness. These results get even more pronounced when we finally address the quantitative goal of winning with a probability in $[0,1]$. We show that for any rational threshold $\theta \in [0,1]$ there is a game that can be won by the protagonist with exactly probability $\theta$ under delayed control, while being surely won by alter in the delay game setting. All these findings refine our original result that games under delayed control are not determined.
翻译:我们比较了延迟控制博弈与延迟博弈,这两种无限博弈模型用于反应式综合中的异步性建模。在延迟控制博弈中,双方玩家因对称延迟通信而遭受部分信息受限;而在延迟博弈中,主角必须向对手玩家授予前瞻视野。我们的第一个主要结果——关于主角必胜策略存在性的相互可归约性——使得能够将延迟博弈中已知的复杂度结果和延迟界限转移到延迟控制博弈中,后者此前并无此类已知结果。我们进一步分析了几乎必然获胜的随机化策略的存在性,此时两类博弈间的对应关系被打破。在此设定下,某些在延迟博弈中对手玩家必胜的博弈,在对应的延迟控制博弈中主角可以几乎必然获胜,这证明主角是否必须授予前瞻视野与双方玩家是否均遭受部分信息受限确实存在差异。当我们最终讨论以$[0,1]$区间内概率获胜的量化目标时,这些结果变得更加显著。我们证明对于任意有理阈值$\theta \in [0,1]$,均存在一个博弈在延迟控制下主角能以恰好概率$\theta$获胜,而在延迟博弈设定中该博弈对手玩家必胜。所有这些发现都深化了我们最初关于延迟控制博弈不具有确定性的结论。