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$获胜的博弈,而该博弈在延迟博弈设定中对手必然获胜。这些发现深化了我们的原始结论——延迟控制下的博弈不具有确定性。