We study turn-based quantitative games of infinite duration opposing two antagonistic players and played over graphs. This model is widely accepted as providing the adequate framework for formalizing the synthesis question for reactive systems. This important application motivates the question of strategy complexity: which valuations (or payoff functions) admit optimal positional strategies (without memory)? Valuations for which both players have optimal positional strategies have been characterized by Gimbert and Zielonka for finite graphs and by Colcombet and Niwi\'nski for infinite graphs. However, for reactive synthesis, existence of optimal positional strategies for the opponent (which models an antagonistic environment) is irrelevant. Despite this fact, not much is known about valuations for which the protagonist admits optimal positional strategies, regardless of the opponent. In this work, we characterize valuations which admit such strategies over infinite game graphs. Our characterization uses the vocabulary of universal graphs, which has also proved useful in understanding recent breakthrough results regarding the complexity of parity games. More precisely, we show that a valuation admitting universal graphs which are monotone and well-ordered is positional over all game graphs, and -- more surprisingly -- that the converse is also true for valuations admitting neutral colors. We prove the applicability and elegance of the framework by unifying a number of known positionality results, proving new ones, and establishing closure under lexicographical products. Finally, we discuss a class of prefix-independent positional objectives which is closed under countable unions.
翻译:我们研究在图上进行的、对抗两名对抗性玩家的无限持续时间回合制量化博弈。该模型被广泛接受为形式化反应式系统综合问题提供适当框架。这一重要应用引出了策略复杂度问题:哪些估值(或收益函数)允许最优位置性策略(无记忆)?对于有限图,Gimbert和Zielonka表征了双方玩家均具有最优位置性策略的估值;对于无限图,Colcombet和Niwiński完成了类似表征。然而,在反应式综合中,对手(模拟对抗性环境)是否存在最优位置性策略并不相关。尽管如此,关于主角(无论对手如何)是否允许最优位置性策略的估值,目前所知甚少。本文中,我们表征了在无限博弈图上允许此类策略的估值。我们的表征使用了泛化图词汇,该词汇已被证明有助于理解奇偶博弈近期突破性结果的复杂性。更具体地说,我们证明:允许单调且良序泛化图的估值在所有博弈图上具有位置性,且——更令人惊讶的是——对于允许中性颜色的估值,其逆命题也成立。我们通过统一若干已知位置性结果、证明新结果以及建立词汇积封闭性,展示了该框架的适用性与优雅性。最后,我们讨论了一类可数并封闭的前缀无关位置性目标。