paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Characterizing Positionality in Games of Infinite Duration over Infinite Graphs

无限图上无限时长博弈中的位置性刻画
LICS Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science2022匹配度 2/10 · 该论文属于逻辑与自动机、无限时长博弈和位置策略的纯理论研究,与形式化合成/验证的理论基础相关,但与用户关注的静态分析、LLM/Agent、浮点程序分析及贝叶斯程序分析没有直接交集。引用 19 inbox
Pierre Ohlmann
crossref: 2026-09-12dblp: 2026-09-12arxiv: 2026-09-12

AI 速览

一句话:用通用图刻画无限图上定量无限时长博弈中允许最优位置策略的赋值,并证明与单调良序通用图存在性的等价(带中性颜色时)。

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

问题
在无限图上的定量无限时长博弈中,哪些赋值(支付函数)能使主角玩家拥有最优位置策略,即不依赖记忆的策略?
方法
作者使用通用图语言,将位置性与单调、良序通用图的存在性联系起来,并对带中性颜色的赋值证明等价刻画。
评估
通过统一已有位置性结果、证明若干更强结论以及确立字典序乘积下的封闭性,展示该框架的适用性与优雅性。
原文摘要(Abstract)

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.

链接与引用

DOI 原文 · arXiv · PDF(开放获取) · DBLP

BibTeX
@inproceedings{Ohlmann23,
  title = {Characterizing Positionality in Games of Infinite Duration over Infinite Graphs},
  author = {Pierre Ohlmann},
  booktitle = {LICS},
  year = {2022},
  doi = {10.1145/3531130.3532418}
}