并发参数化博弈的反链
Antichains for Concurrent Parameterized Games
查看机构详情
- Universit\'e de Rennes, Inria, CNRS, IRISA, Rennes, France
- LMF, CNRS \& ENS Paris-Saclay,\ \'e Paris-Saclay, Gif-sur-Yvette, France
机构由 AI 辅助整理，请以论文原文为准。
浏览论文内容
中文总结 AI 辅助
针对并发参数化可达性博弈的Eve获胜区域问题，提出基于反链的符号方法及两个不动点算法，实现后在基准测试中验证了性能。
中文摘要 AI 辅助
并发参数化博弈涉及固定但任意数量的玩家，由有限竞技场描述，其中边用语言标记，这些语言描述从一个顶点到另一个顶点的可能移动组合（n个玩家对应长度为n的单词）。此前研究表明，当边标记为正则语言时，可判定名为Eve的指定玩家是否存在策略，以对抗任意多对手的任意策略组合，确保可达性目标，该判定问题是PSPACE完全的。PSPACE成员证明的一个基本要素是归约为指数规模的知识博弈，这是一种2玩家博弈，反映Eve对对手数量的认知。本文提出一种基于反链的符号方法，用于计算知识博弈中Eve的获胜区域，即给出Eve在每个顶点获胜所需的最小认知。更准确地说，我们提出两个不动点算法，以反链形式计算知识博弈中Eve获胜区域的最大元素。我们用C++实现了这两个算法及最初提出的算法，并报告了它们在各种基准测试上的相对性能。
英文摘要
Concurrent parameterized games involve a fixed yet arbitrary number of players. They are described by finite arenas in which the edges are labeled with languages that describe the possible move combinations leading from one vertex to another (n players yield a word of length n). Previous work showed that, when edge labels are regular languages, one can decide whether a distinguished player, called Eve, has a strategy to ensure a reachability objective, against any strategy profile of her arbitrarily many opponents. This decision problem is known to be PSPACE-complete. A basic ingredient in the PSPACE-membership proof is the reduction to the exponential-size knowledge game, a 2-player game that reflects the knowledge Eve has on the number of opponents. In this paper, we provide a symbolic approach, based on antichains, to compute Eve's winning region in the knowledge game. In words, it gives the minimal knowledge Eve needs at every vertex to win the concurrent parameterized reachability game. More precisely, we propose two fixed-point algorithms that compute, as an antichain, the maximal elements of the winning region for Eve in the knowledge game. We implemented these two algorithms in C++, as well as the one initially proposed, and report on their relative performances on various benchmarks.
