提示延迟

摘要：

延迟博弈是两个玩家的博弈，其中一个玩家可以延迟她的行动，以获得对对手行动的前瞻。近年来，人们对弱MSO中具有量化获胜条件的无界量词博弈进行了研究，但其性质并不令人满意。特别是，无界前瞻一般是必要的。在这里，我们研究了延迟博弈的获胜条件给出的LTL，线性时序逻辑配备了一个参数化的最终运营商，其范围是有界的。我们的主要结果表明，解决的三重指数时间的LTL延迟对策是完全的。此外，我们给出了严格的三重指数界上的必要的前瞻性和参数化的最终运营商的范围。因此，我们确定的第一类行为良好的定量获胜条件延迟游戏的LTL。最后，我们表明，应用我们的技术，延迟游戏与ω-正规的获胜条件回答开放的问题的情况下，获胜的条件是由非确定性的，通用的，或交替自动机。

英文摘要：

Delay games are two-player games of infinite duration in which one player may delay her moves to obtain a lookahead on her opponent's moves. Recently, such games with quantitative winning conditions in weak MSO with the unbounding quantifier were studied, but their properties turned out to be unsatisfactory. In particular, unbounded lookahead is in general necessary. Here, we study delay games with winning conditions given by Prompt-LTL, Linear Temporal Logic equipped with a parameterized eventually operator whose scope is bounded. Our main result shows that solving Prompt-LTL delay games is complete for triply-exponential time. Furthermore, we give tight triply-exponential bounds on the necessary lookahead and on the scope of the parameterized eventually operator. Thus, we identify Prompt-LTL as the first known class of well-behaved quantitative winning conditions for delay games. Finally, we show that applying our techniques to delay games with ω-regular winning conditions answers open questions in the cases where the winning conditions are given by non-deterministic, universal, or alternating automata.

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。