一句话:用通用图刻画无限图上定量无限时长博弈中允许最优位置策略的赋值,并证明与单调良序通用图存在性的等价(带中性颜色时)。
本文研究图上由两个对抗玩家进行的回合制定量无限时长博弈;该模型被广泛用于形式化反应式系统的合成问题。核心问题是策略复杂度:哪些赋值(支付函数)允许最优位置策略(即无记忆策略)?已有工作刻画了双方均有最优位置策略的赋值,但反应式合成只关心主角玩家能否无视对手而采用最优位置策略。作者在无限图上刻画此类赋值,采用通用图(universal graphs)语言:证明若赋值允许单调且良序的通用图,则它在所有博弈图上是位置性的;更令人惊讶的是,对带有中性颜色的赋值,逆命题也成立。该框架统一并加强了若干已知位置性结果,并证明在字典序乘积下封闭。
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 [16] for finite graphs and by Colcombet and Niwiński [12] 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 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 monotonic 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 a few stronger ones, and establishing closure under lexicographical products.