一句话：该论文将数据词上重复值逻辑的博弈问题与能量游戏及带状态向量加法系统联系起来，并给出可判定片段。
本文研究在无限数据域上生成多属性数据词的双人博弈，玩家轮流为变量选取无限数据域中的取值，胜负由重复值逻辑公式判定，该逻辑可表达无限数据词中数据值的重复关系。作者证明，即使在对博弈施加很强限制的情况下，判断某一玩家是否存在获胜策略也是不可判定的。主要正面结果：若将其中一名玩家的取值限制在布尔域，则此类博弈可有效等价为带状态的向量加法系统上的单边博弈（一方可改变控制状态但不能改变计数值），后者已知可判定，并等价于能量游戏。该结果把重复值逻辑可满足性与向量加法系统可达/覆盖性之间的已知联系提升到博弈层面。
We introduce two-player games which build words over infinite alphabets, and we study the problem of checking the existence of winning strategies. These games are played by two players, who take turns in choosing valuations for variables ranging over an infinite data domain, thus generating multi-attributed data words. The winner of the game is specified by formulas in the Logic of Repeating Values, which can reason about repetitions of data values in infinite data words. We prove that it is undecidable to check if one of the players has a winning strategy, even in very restrictive settings. However, we prove that if one of the players is restricted to choose valuations ranging over the Boolean domain, the games are effectively equivalent to single-sided games on vector addition systems with states (in which one of the players can change control states but cannot change counter values), known to be decidable and effectively equivalent to energy games. Previous works have shown that the satisfiability problem for various variants of the logic of repeating values is equivalent to the reachability and coverability problems in vector addition systems. Our results raise this connection to the level of games, augmenting further the associations between logics on data words and counter systems.
@article{paperbot1008,
title = {Playing with Repetitions in Data Words Using Energy Games},
author = {Diego Figueira and Anirban Majumdar and M. Praveen},
journal = {Logical Methods in Computer Science},
volume = {Volume 16, Issue 3},
year = {2020},
doi = {10.23638/lmcs-16(3:1)2020}
}