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 even over infinite 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\'nski 为无限的图形提供。 然而, 对于反应合成而言, 对手( 模拟对立环境) 存在最佳定位战略是无关的。 尽管这一事实, 但对于主要玩家接受最佳定位战略( 或报酬功能) 接受最佳定位战略( 没有记忆 ) 的复杂战略( 没有记忆 )? 在这项工作中, 我们的定性使用了通用图表的词汇, 这也有助于理解关于均等游戏复杂性的近期突破性结果。 更准确地说, 我们显示, 一个承认通用图表的通用图表是单数和正确度, 在游戏的透明性定义框架下,, 我们的定型的定型的定型的定型的定型的定型的定型的定型的定型是 。