利用能量游戏对数据字中的重复进行处理
摘要：存在哪个玩家有获胜策略的问题是我们引入的构建无限字母表上单词的双人游戏的研究。这些游戏由两个玩家玩，他们轮流选择对无限数据领域变量的评估，从而生成多属性数据单词。游戏的获胜者由Logic of Repeating Values中的公式指定，该公式可以推理无限数据单词中数据值的重复。我们证明，在非常限制的情况下，检查其中一个玩家是否有获胜策略是不可判定的。然而，我们证明，如果其中一个玩家被限制在选择布尔领域变量的评估上，那么这些游戏就可以有效地等价于具有状态的向量加法系统上的单边游戏（其中一个玩家可以改变控制状态但不能改变计数器值），已知可判定且与能量游戏有效等价。 先前的研究表明，重复值逻辑的各种变体的可满足性问题等价于向量加法系统中的可达性和覆盖性问题。我们的结果将这种关联提升到游戏的层面，进一步增强了数据单词和计数器系统之间的关联。
作者：Diego Figueira, Anirban Majumdar and M. Praveen
论文ID：1802.07435
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-06-22