Parity Games with Weights
本文研究带任意整数权重的奇偶博弈,证明其求解属于NP∩coNP,主角有有限状态策略且内存有紧致伪多项式界,并证明阈值问题为EXPTIME-完全。
2019-08-22 cs.GT cs.LO
Attracting Tangles to Solve Parity Games
奇偶博弈在形式化验证和综合中有重要的实际应用,特别是在解决模态μ演算的模型检验问题上。从理论的角度来看,它们也很有趣,因为它们被广泛认为是多项式解,但到目前为止还没有这样的算法。我们提出了一个新的算法来解决基于学习缠结,这是强连接的子图,其中一个玩家有一个策略,赢得所有的循环在子图的奇偶游戏。我们认为,缠结发挥了重要的作用,在突出的奇偶博弈求解算法。我们证明了缠结学习在实践中是有竞争力的,并且是大型随机游戏的最快求解器。
2018-04-14 cs.GT cs.LO
Winning Cores in Parity Games
我们在奇偶博弈中引入了赢核的新概念,并在赢核近似的基础上提出了一个求解奇偶博弈的确定性多项式时间下近似算法。该算法的基础是一些关于赢得核心的属性,这些属性本身就很有趣。特别是,我们证明了在一个平价博弈中,一个玩家的获胜核心和获胜区域是等价的。此外,获胜的核心包含所有致命吸引子,但不一定是一个统治。实验结果是非常积极的两个方面的质量近似和运行时间。在大多数基准测试中,它的性能明显优于现有的最先进的算法。
2016-02-05 cs.GT cs.LO
A Parity Game Tale of Two Counters
奇偶博弈是在有限图上进行的简单的无限博弈,其获胜条件具有足够的表现力以捕获嵌套的最小和最大不动点。通过它们与模态μ演算的紧密关系,它们在实践中用于μ演算以及相关时态逻辑(例如LTL和CTL)的模型检查和综合问题。解决奇偶博弈是一个引人注目的复杂性理论问题,因为该问题位于UP和co-UP的交叉点,并且被认为是多项式时间的解决方案,激励研究人员找到这样的解决方案或找到现有算法的超多项式下界,以提高对奇偶博弈的理解。我们提出了一个参数化的奇偶性游戏称为两个计数器的游戏,它提供了一个指数下界的吸引子为基础的奇偶性游戏求解算法。我们是第一个为延迟提升策略的优先级提升提供指数下限的人,也是第一个为缠结学习提供这样的下限的人。
2019-09-17 cs.GT cs.LO
Alpaga: A Tool for Solving Parity Games with Imperfect Information
Alpaga是一个求解不完全信息的两人平价博弈的算法。给定博弈的描述,它确定第一个参与者是否能确保获胜,如果是,它构造获胜策略。该工具提供了一个基于反链的最新算法的符号实现。
2009-01-29 cs.GT cs.LO
Stochastic Parity Games on Lossy Channel Systems
我们给出了一个算法,用于解决随机奇偶游戏的几乎肯定的获胜条件,在有损耗的信道系统中的情况下,球员被限制到有限的记忆策略。首先,我们描述了一个一般的框架,在那里我们考虑类的2.5玩家的游戏几乎肯定的奇偶性获胜的条件可能是无限的游戏图,假设游戏包含一个有限的吸引子。吸引子是一组状态(不一定是吸收的),无论参与者的决定如何,它几乎肯定会被重新访问。我们提出了一个方案,其特征在于为每个玩家的获胜状态集。然后,我们实例化这个计划,以获得一个算法的随机博弈有损信道系统。
2013-06-13 cs.GT cs.LO
Oink: an Implementation and Evaluation of Modern Parity Game Solvers
奇偶博弈在形式化验证和综合中有重要的实际应用,特别是在解决模态μ演算的模型检验问题上。从理论的角度来看,它们也很有趣,因为它们被广泛认为是多项式解,但到目前为止还没有这样的算法。近年来,提出了许多新的算法和对现有算法的改进。我们实现了一个新的,易于扩展的工具Oink,这是一个高性能的现代奇偶博弈算法的实现。我们进一步提出了一个全面的经验评估现代平价游戏算法和求解器,无论是在现实世界的基准和随机生成的游戏。我们的实验表明,我们的新工具Oink优于目前的国家的最先进的。
2018-03-05 cs.GT cs.LO
Generating and Solving Symbolic Parity Games
我们提出了一个新的工具,验证模态μ演算公式的过程规范,基于符号奇偶游戏。它增强了现有的方法,首先编码的问题的参数化布尔方程系统(PBES),然后实例化PBES的奇偶性游戏。我们改进了从规范到PBES的转换以保持PBES中规范的结构,我们扩展了LTSmin以将PBES实例化为符号奇偶博弈,并实现了Zielonka的符号奇偶博弈递归求解算法。我们使用多值决策图(MDDs)来表示集合和关系,从而使工具能够处理非常大的系统。基于规范的结构划分转换关系,这允许有效地操纵MDD。我们进行了两个案例研究的模块化规范,表明新方法具有更好的时间和内存性能比现有的PBES为基础的工具,可以更快(但略低于内存效率)比符号模型检查NuSMV。
2014-07-30 cs.GT cs.LO
Simple Stochastic Games with Almost-Sure Energy-Parity Objectives are in NP and coNP
我们研究随机游戏的能量平价的目标,结合定量奖励与定性$ω$定期条件:最大化的目的是避免耗尽能量,同时满足奇偶条件。我们表明,相应的几乎肯定的问题,即,检查是否存在最大化器策略,该最大化器策略在以给定能量水平$k$开始时以概率$1$实现能量奇偶性目标是可判定的并且在$NP \cap coNP$中。这同样适用于检查这样的$k$是否存在以及给定的$k$是否最小。
2021-01-18 cs.GT cs.LO
Timed Parity Games: Complexity and Robustness
我们考虑两个玩家的游戏在实时的时钟和奇偶性目标的游戏结构。游戏是并行的,在每一轮,两个玩家独立地提出一个时间延迟和一个动作,并选择具有较短延迟的动作。为了防止玩家通过阻塞时间来获胜,我们限制每个玩家的策略,以确保玩家不能对导致zeno运行负责。首先,我们提出了一个有效的减少这些游戏回合制(即,非并发)有限状态(即,不定时的)平价游戏。结果游戏的状态是原始游戏的时钟区域对。我们的减少提高了最有名的复杂性解决定时奇偶游戏。此外,经典奇偶博弈的丰富算法现在可以应用于定时奇偶博弈。其次,我们考虑两个限制类的策略的球员,代表控制器在一个实时的综合问题,即有限的鲁棒和有界的鲁棒策略。使用极限鲁棒策略,控制器不能选择精确的实值时间延迟,但必须允许在其每个动作中存在一些非零抖动。如果抖动有一个给定的下限,那么该策略是有界鲁棒的。我们证明了精确策略比极限鲁棒策略更强大,极限鲁棒策略比有界鲁棒策略更强大。对于这两种强大的战略,我们提出了有效的减少标准的时间自动机游戏。这些减少提供了鲁棒实时控制器的合成算法。
2008-07-08 cs.GT cs.LO
Banach-Mazur Parity Games and Almost-sure Winning Strategies
两人随机博弈是两个2人和一个被称为“自然”的随机实体的博弈。在这个框架中,一个自然的问题是确保事件发生概率为1的策略(几乎肯定策略)的存在。在马尔可夫决策过程的情况下,当感兴趣的事件2作为奇偶条件给出时,我们可以用两个以上的参与者来代替“自然”,这些参与者根据所谓的Banach-Mazur游戏规则进行游戏[1]。在本文中,我们继续这一研究计划,将上述结果扩展到两个玩家的随机奇偶游戏。与文献[1]中一样,基本思想是,在正确的假设下,我们可以用两个参与者进行Banach-Mazur博弈来代替随机参与者。这需要一些技术性的观察,和一个不平凡的证明,这篇论文开始做。
2018-06-26 cs.GT cs.LO
Window Parity Games: An Alternative Approach Toward Parity Games with Time Bounds
图上两人零和博弈的经典目标通常处理无限博弈的极限行为:例如,在定量环境中的平均收益和总收益,或在定性环境中的奇偶性(编码Ω正则性质的规范方法)。这些目标提供了强大的抽象机制,并经常产生良好的属性,如无记忆的确定性。然而,它们的性质本身并不能保证在一定的时间范围内可以看到一些好的东西。在这项工作中,我们考虑两种方法对包含时间界限的奇偶性游戏。第一个是奇偶反应博弈,它是基于有限奇偶博弈[CHH 09]和有成本的奇偶博弈[FZ 14,WZ 16]的概念。第二个是窗口平价博弈,它的灵感来自于窗口平均收益博弈[CDRR 15]。我们比较了这两种方法,并表明,虽然它们被证明是等价的,在某些情况下,窗口奇偶校验游戏提供了一个更容易处理的替代方案时,时间界限作为一个参数(P-C。vs. PSPACE-c.)。特别是,它提供了一个保守的近似奇偶游戏可计算的多项式时间。此外,我们将这两种方法扩展到多维设置。我们给这两种类型的游戏的复杂性和内存边界的全貌。[CHH09] K. Chatterjee,T.A. Henzinger,F. Horn(2009):在omega常规游戏中最终获胜。ACM Trans. Comput. Log. 11(1). [FZ14] N. Fijalkow,M. Zimmermann(2014):Parity and Streett Games with Costs. LMC…
2016-09-14 cs.FL cs.GT cs.LO
Postinal Determinacy of Games with Infinitely Many Priorities
我们研究两个玩家的游戏无限的持续时间,有限或无限的游戏图。对于这样一个博弈,如果获胜策略只取决于当前的位置,而不取决于博弈的历史,那么它就是位置策略。一个博弈是由位置决定的,如果在每个位置上,两个玩家中的一个有位置获胜策略。这类博弈的理论在获胜条件方面得到了很好的研究,获胜条件是根据映射来定义的,该映射从有限集合中为每个位置分配优先级。具体来说,在穆勒博弈中,一局的赢家是由那些出现频率无限高的优先级的集合决定的;一个重要的特例是奇偶博弈,其中出现频率无限高的最小(或最大)优先级决定赢家。众所周知,平价游戏是由位置决定的,而穆勒游戏是通过有限记忆策略决定的。在本文中,我们将这个理论扩展到无限多个优先级的博弈的情况。这样的游戏出现在几个应用领域,例如在下推游戏中,获胜条件取决于堆栈内容。对于奇偶博弈,有几种对无穷多个优先级的情况的概括。虽然最大奇偶游戏在欧米茄或最小奇偶游戏在更大的序数比欧米茄需要的战略与无限的记忆,我们可以证明,最小奇偶游戏的优先级在欧米茄是位置确定的。事实上,事实证明,最小奇偶条件在欧米茄是唯一的无穷穆勒条件,保证位置确定性的所有游戏图。
2012-08-28 cs.GT cs.LO
Positional Determinacy of Games with Infinitely Many Priorities
我们研究两个玩家的游戏无限的持续时间,有限或无限的游戏图。对于这样一个博弈,如果获胜策略只取决于当前的位置,而不取决于博弈的历史,那么它就是位置策略。一个博弈是由位置决定的,如果在每个位置上,两个玩家中的一个有位置获胜策略。这类博弈的理论在获胜条件方面得到了很好的研究,获胜条件是根据映射来定义的,该映射从有限集合中为每个位置分配优先级。具体来说,在穆勒博弈中,一局的赢家是由那些出现频率无限高的优先级的集合决定的;一个重要的特例是奇偶博弈,其中出现频率无限高的最小(或最大)优先级决定赢家。众所周知,平价游戏是由位置决定的,而穆勒游戏是通过有限记忆策略决定的。在本文中,我们将这个理论扩展到无限多个优先级的博弈的情况。这样的游戏出现在几个应用领域,例如在下推游戏中,获胜条件取决于堆栈内容。对于奇偶博弈,有几种对无穷多个优先级的情况的概括。虽然最大奇偶游戏在欧米茄或最小奇偶游戏在更大的序数比欧米茄需要的战略与无限的记忆,我们可以证明,最小奇偶游戏的优先级在欧米茄是位置确定的。事实上,事实证明,最小奇偶条件在欧米茄是唯一的无穷穆勒条件,保证位置确定性的所有游戏图。
2006-11-03 cs.GT cs.LO
Window Parity Games: An Alternative Approach Toward Parity Games with Time Bounds (Full Version)
图上两人零和博弈的经典目标通常处理无限博弈的极限行为:例如,在定量环境中的平均收益和总收益,或在定性环境中的奇偶性(编码Ω正则性质的规范方法)。这些目标提供了强大的抽象机制,并经常产生良好的属性,如无记忆的确定性。然而,它们的性质本身并不能保证在一定的时间范围内可以看到一些好的东西。在这项工作中,我们考虑两种方法对包含时间界限的奇偶性游戏。第一个是奇偶反应博弈,它是基于有限奇偶博弈[CHH 09]和有成本的奇偶博弈[FZ 14,WZ 16]的概念。第二个是窗口平价博弈,它的灵感来自于窗口平均收益博弈[CDRR 15]。我们比较了这两种方法,并表明,虽然它们被证明是等价的,在某些情况下,窗口奇偶校验游戏提供了一个更容易处理的替代方案时,时间界限作为一个参数(P-C。vs. PSPACE-C.)。特别是,它提供了一个保守的近似奇偶游戏可计算的多项式时间。此外,我们将这两种方法扩展到多维设置。我们给这两种类型的游戏的复杂性和内存边界的全貌。[CHH09] K. Chatterjee,T.A. Henzinger,F. Horn(2009):在omega常规游戏中最终获胜。ACM trans. comput. log. 11(1). [FZ14] N. Fijalkow,M. Zimmermann(2014):Parity and Streett Games with Costs. LMC…
2016-09-15 cs.FL cs.GT cs.LO
The Complexity of Partial-observation Stochastic Parity Games With Finite-memory Strategies
我们考虑有限状态图上的两个局中人部分观察随机博弈,其中局中人1有部分观察,局中人2有完美观察。我们研究的获胜条件是指定为宇称目标的ω-正则条件。给定一个部分观察随机博弈和一个奇偶目标的定性分析问题是,是否存在一个策略来确保目标以概率~1(分别为1和2)满足。正概率)。这些定性分析问题是已知的不可判定的。然而,在许多应用程序的相关问题是有限记忆策略的存在,和有限记忆策略下的定性分析问题最近被证明是可判定的2 EXPTIME。我们提高了复杂性,并表明,定性分析问题的部分观察随机奇偶游戏有限记忆策略下的EXPTIME-完全的,也建立了最佳的(指数)记忆边界所需的定性分析有限记忆策略。
2014-01-14 cs.GT cs.LO
Easy to Win, Hard to Master: Optimal Strategies in Parity Games with Costs
本研究探讨带成本的奇偶博弈中的最优策略,发现求解最小成本界限的策略问题为PSPACE完全,且指数级内存必要且充分,表明最优求解比仅获胜更难,并研究了内存与界限间的渐进权衡及带成本Streett博弈的最优性。
2017-09-18 cs.GT cs.LO
Parity games and universal graphs
本文是一个贡献的研究奇偶游戏和最近的建设三个拟多项式时间算法来解决他们。我们重新审视Czerwienski,Daviaud,Fijalkow,Jurdzienski,Lazić和Parys的结果,见证了所有三个拟多项式时间算法的拟多项式障碍。论证了这三种算法都可以理解为构造一个所谓的分离自动机,并给出了关于分离自动机大小的一个拟多项式下键。我们给出了这个结果的另一种证明。本文的主要创新点是泛图的概念和饱和度的思想。
2018-10-19 cs.GT cs.LO
Quasipolynomial Set-Based Symbolic Algorithms for Parity Games
求解等价于模态$μ$ -演算模型检验的奇偶博弈是形式化方法中的一个核心算法问题。除了标准的计算模型与明确表示的游戏,另一个重要的理论模型的计算是基于集合的符号算法。基于集合的符号算法使用基本集合运算和一步前置运算对博弈进行隐式描述,而不是显式表示。符号算法的意义在于,它们为大型有限状态系统以及具有有限商的无限状态系统提供了可扩展的算法。考虑具有$n$顶点和具有$d$优先级的奇偶性条件的图上的奇偶性博弈。虽然有丰富的文献显式算法的奇偶游戏,基于集合的符号算法的主要结果如下:(a)一个算法,需要$O(n^d)$符号操作和$O(d)$符号空间;(b)一个改进的算法,需要$O(n^{d/3+1})$符号操作和$O(n)$符号空间。本文的主要工作如下:(1)在显式进度度量算法的基础上,提出了一种基于黑箱集合的符号算法。我们的算法的两个重要的后果如下:(a)基于集合的符号算法的奇偶游戏,需要准多项式许多符号操作和$O(n)$符号空间;和(b)任何未来的改进,基于进度测量的显式算法意味着我们的基于集合的符号算法的奇偶游戏的效率提高。(2)我们提出了一个基于集合的符号算法,需要准多项式的许多符号运算和$O(d \cdot \log n)$符号空间。此外,对于$d \leq \log n$这一重要的特殊情况,我们的算法只需要多项式的符号运算和多对数符号空间。
2019-09-11 cs.GT cs.LO
A pseudo-quasi-polynomial algorithm for solving mean-payoff parity games
在平均收益平价博弈中,两个博弈者中的一个既要实现定性的平价目标,又要最小化定量的长期平均收益(又名。平均收益)。游戏是零和的,因此另一个玩家的目标是要么挫败平价目标,要么最大化平均收益。我们的主要技术成果是一个伪拟多项式算法求解平均支付平价游戏。所有的算法已经开发了十多年的问题有一个伪多项式和指数因子在他们的运行时间;在我们的算法的运行时间,后者被替换为一个准多项式。根据Chatterjee和Doyen(2012)以及Schewe,Weinert和Zimmermann(2018)的结果,我们的主要技术结果意味着存在用于求解奇偶能量博弈和求解具有权重的奇偶博弈的伪准多项式算法。我们的主要概念的贡献是双方球员的战略分解的定义,和一个概念的进展措施的平均回报平价游戏,推广平价和能源的进展措施。前者提供了范式和简洁的表示获胜的策略,后者使应用程序的平均支付奇偶游戏的顺序理论的机器,支持最近的准多项式算法解决奇偶游戏。
2018-07-10 cs.DS cs.GT cs.LO
Efficient Instantiation of Parameterised Boolean Equation Systems to Parity Games
参数化布尔方程系统(PBES)是具有数据变量的布尔定点方程的序列,用于例如,用数据验证过程代数规范的模态μ演算公式。解决PBES通常通过实例化到奇偶博弈然后解决博弈来完成。实际的游戏求解器是存在的,但实例化步骤是瓶颈。我们分两步增强实例化。首先,我们将PBES转换为一个参数化奇偶博弈(PPG),一个PBES与每个方程的合取或析取。然后,我们使用LTSmin,提供过渡缓存,有效的存储状态和分布式和符号状态空间生成,用于生成游戏图。为此,我们定义了一个语言模块的LTSmin,由一个编码的变量与参数到状态向量,一个分组的过渡关系和一个依赖矩阵,以表示部分的状态向量和过渡组之间的依赖关系。一些大型案例的基准测试表明,该方法大大加快了实例化的速度,并大大减少了内存使用。
2012-10-24 cs.GT cs.LO
Partial Solvers for Generalized Parity Games
近年来,奇偶博弈在控制器综合和验证中的应用得到了广泛的研究。实际上,在多项式时间内执行的奇偶博弈的部分求解器虽然不完整,但可以解决公开可用的基准套件中的大多数博弈。在本文中,我们结合这些部分求解器与经典的递归算法的奇偶游戏由于Zielonka。我们还将部分求解器扩展到广义奇偶性游戏,即奇偶性目标结合的游戏。我们已经实现了这些算法,并评估了他们在最后一个LTL合成比赛中提出的一个大型基准。
2019-07-20 cs.GT
Reachability Games and Parity Games
奇偶博弈是由位置决定的。这是一个基本的和经典的结果。2010年,Calude等人展示了有限奇偶博弈的突破性结果:获胜区域及其位置获胜策略可以在准多项式时间内计算。本文对这两个结果给出了完备的详细证明。本文中的结果并不意味着是原创的。位置的确定性结果显示可能无限的奇偶性游戏使用的想法Zielonka,他在1998年出版。为了展示准多项式时间,我们遵循Lehtinen在2018年介绍的寄存器游戏。虽然Lehtinen算法的时间复杂度不是最优的,但寄存器游戏本身在概念上是简单而有趣的。我们的各种证明要么是新的,要么是原始证明的简化。本文的主题包括可达对策的最优吸引子的定义和计算。
2022-08-22 cs.FL cs.GT cs.LO
Faster Algorithms for Mean-Payoff Parity Games
图游戏为反应过程的建模和综合提供了基础。这种游戏是在图上进行的,其中顶点由两个敌对的玩家控制。我们考虑图游戏的第一个玩家的目标是一个定性目标(指定为奇偶条件)和定量目标(指定为平均回报条件)的结合。这个问题有两种变体,即阈值问题,其中定量目标是确保平均收益值高于阈值,以及价值问题,其中定量目标是确保最佳平均收益值;在这两种情况下,都确保定性平价目标。对于具有$n$顶点、$m$边、具有$d$优先级的奇偶目标以及用于平均支付目标的最大绝对奖励值$W$的博弈图,先前最著名的算法如下:用于阈值问题的$O(n^{d+1} \cdot m \cdot W)$,以及用于值问题的$O(n^{d+2} \cdot m \cdot W)$。我们的主要贡献是更快的算法,我们的算法的运行时间如下:$O(n^{d-1} \cdot m \cdot W)$的阈值问题,和$O(n^{d} \cdot m \cdot W \cdot \log (n\cdot W))$的价值问题。对于具有两个优先级的平均收益奇偶目标,我们的算法与平均收益游戏的算法的最知名的界限相匹配(不与奇偶目标相结合)。我们的结果与具有功能要求(作为定性目标给出)和性能要求(作为定量目标给出)的反应系统的合成相关。
2017-06-19 cs.GT cs.LO
A Compositional Approach to Parity Games
在本文中,我们介绍了开放的平价游戏,这是一个组合的方法平价游戏。这是通过在通常的平价博弈概念上增加开放式结局来实现的。我们介绍了开放的奇偶游戏,这是使用标准定义的图形游戏的类别。我们还定义了一个图形语言的开放奇偶校验游戏作为道具,最近已被用于许多应用程序中的图形语言。我们引入了一个合适的语义类别的启发工作Grellois和Melliès的语义高阶模型检验。计算开放奇偶博弈中获胜位置的集合产生语义范畴的函子。最后,通过解释图形语言的语义范畴,我们表明,这种计算可以进行组合。
2021-12-28 cs.GT
Playing Pushdown Parity Games in a Hurry
我们继续调查的有限持续时间的无限持续时间的游戏扩展到无限的游戏的有限持续时间的变种。特别是,我们建立了一个等价的下推平价游戏和有限持续时间的变体。这使我们能够通过在有限树上求解可达性博弈来确定下推奇偶博弈的获胜者。
2012-10-09 cs.GT
From Local To Global Optimality in Concurrent Parity Games
本文研究了有限图上的双人并发随机奇偶博弈,提出了一个在每个状态满足时即可保证双方玩家均存在位置最优策略的局部结构条件。
2023-11-24 cs.GT
Strategy Iteration using Non-Deterministic Strategies for Solving Parity Games
本文将通过策略迭代解决奇偶博弈的思想扩展到非确定性策略:在非确定性策略中,参与者将自己限制在给定节点上可能行动的非空子集,而不是将自己限制在一个行动上。我们表明,Bjoerklund,桑德伯格和Vorobyov的策略改进算法可以很容易地适应更一般的设置的非确定性策略。此外,我们表明,应用启发式的“所有有利可图的开关”导致选择一个“局部最优”的继任者的战略设置的非确定性的战略,从而获得一个简单的证明Schewe的算法。与Bjoerklund等人的算法相反,我们提出了我们的算法直接为平价游戏,使我们能够比较它的算法由Jurdzinski和Voege:我们表明,在这两种算法中使用的估值一致的平价游戏竞技场,其中一个球员可以“投降”。因此,我们的算法也可以被看作是一个推广的Jurdzinski和Voege的非确定性策略。最后,使用非确定性策略使我们能够证明改进步骤的数量由O(1.724^n)约束。对于策略改进算法,这个界限以前只知道可以通过使用随机化来实现。
2012-03-19 cs.GT cs.LO
Doubly Fair Parity Games
University of Liverpool(利物浦大学);University of Gothenburg(哥德堡大学);Chalmers University of Technology(查尔姆斯理工大学);Max Planck Institute for Software Systems (MPI-SWS)(马克斯·普朗克软件系统研究所)
本文研究了双玩家有限图游戏中的公平性约束,提出公平α/β游戏模型,并通过构造技巧将公平奇偶游戏转化为普通奇偶游戏,同时给出直接的符号固定点算法。
2026-05-11 cs.GT
Algorithm and Strategy Construction for Sure-Almost-Sure Stochastic Parity Games
Université Paris-Saclay, CNRS, ENS Paris-Saclay, LMF(巴黎萨克雷大学、法国国家科学研究中心、巴黎萨克雷高等师范学院、拉格朗日数学物理实验室);Tata Institute of Fundamental Research(塔塔基础研究所)
本文提出了一种递归算法,用于构造确保和几乎确保随机奇偶游戏的获胜策略,并推导了特殊类别的复杂性和内存界限。
2026-01-06 cs.GT cs.LO
A reduction from parity games to simple stochastic games
图上的博弈为反应式非终止系统提供了一个自然的模型。在这样的游戏中,两个玩家在竞技场上的交互导致描述系统运行的无限路径。在计算机科学中,不同的设置被用来对各种开放系统进行建模,例如基于回合或并发的移动,以及确定性或随机性的转换。在本文中,我们感兴趣的回合制游戏,特别是在确定性奇偶游戏和随机可达性游戏(也称为简单随机游戏)。我们提出了一个简单的,直接的和有效的减少从确定性奇偶游戏简单的随机游戏:它产生一个舞台的大小是线性的对数因子的原始舞台的大小。
2011-06-07 cs.GT
Faster Game Solving by Fixpoint Acceleration
提出通过计算DAG吸引子函数的嵌套不动点加速求解具有无环子结构的奇偶博弈,并设计经济构造将Emerson-Lei博弈转化为奇偶博弈以实现加速求解。
2025-11-04 cs.GT cs.LO
Time Flies When Looking out of the Window: Timed Games with Window Parity Objectives
窗口机制是由Chatterjee等人引入的,用于在图上的两人回合制游戏中加强具有时间界限的平均支付和总支付目标。从那以后,它被证明在各种环境中都很有用,包括游戏中的奇偶性目标和马尔可夫决策过程中的平均收益和奇偶性目标。我们研究时间自动机和定时游戏中的窗口奇偶性目标:给定窗口大小的界限,如果在路径上的所有状态中,我们看到一个足够小的窗口,其中最小的优先级是偶数,则路径满足这样的目标。我们发现,检查时间自动机的所有时间发散路径满足这样的窗口奇偶校验目标可以在多项式空间中完成,并且相应的时间游戏可以在指数时间内求解。这与计时奇偶游戏的复杂性相匹配,同时增加了推理时间界限的能力。我们还考虑了多维目标,并表明复杂性类不会增加。据我们所知,这是第一次在实时设置中研究窗口机制。
2021-08-11 cs.FL cs.GT cs.LO
Value Iteration for Stochastic Parity Games
National Institute of Informatics(国立情报学研究所);SOKENDAI (The Graduate University for Advanced Studies)(综合研究大学院大学);Imiron Co., Ltd.(Imiron有限公司)
针对随机奇偶博弈的定量分析,提出首个值迭代算法,该算法直接基于获胜概率的格理论表征操作,利用相关结构特性,与基于策略迭代的现有算法不同,还证明了算法的正确性和收敛性。
2026-07-23 cs.GT
Local Strategy Improvement for Parity Game Solving
奇偶博弈的求解问题是模型检验、可满足性检测和程序合成中许多问题的核心。解决奇偶博弈的一些最好的算法是策略改进算法。这些都是全球性的,因为它们需要整个平价博弈在一开始就存在。这是一个明显的缺点,因为在许多应用中,人们只需要知道特定节点属于哪个获胜区域,并且见证获胜策略可能只覆盖整个游戏图的一小部分。我们提出了一个局部策略改进算法,该算法在执行改进步骤的同时探索游戏图。我们还比较了它与现有的全局策略改进算法和目前唯一的其他局部算法解决奇偶博弈的经验。事实证明,局部策略改进可以超过其他策略几个数量级。
2010-06-08 cs.CC cs.DS cs.GT
Solving 3-Color Parity Games in $ O(n^2) $ Time
奇偶博弈是一个考虑omega-正则语言可实现性问题的表达框架。然而,它是开放的,他们是否可以解决在多项式时间,使他们不适合实际使用。为了克服这个限制,我们考虑3色奇偶博弈,它可以在多项式时间内求解。它们仍然覆盖了规范的表达片段,因为它们包括经典的Büchi和co-Büchi获胜条件以及它们的并集和交集。这已经足以表达安全性和活性性质的许多有用组合,例如GR(1)族。最著名的三色奇偶博弈算法在$ O(n^{2}\sqrt{n}) $时间内解决了一个有n个顶点的博弈。我们提出了一个新的算法,基于简单的吸引子结构,这只需要时间$ O(n^2) $,从而改善了这一结果。因此,我们匹配最知名的运行时间解决(共)-Büchi游戏,表明3色奇偶性游戏并不难解决一般。
2014-12-19 cs.FL cs.GT cs.LO
Universal Algorithms for Parity Games and Nested Fixpoints
给出了一种用于求解奇偶博弈的吸引子分解元算法,该算法推广了经典的McNaughton-Zielonka算法及其最近的准多项式变体,这些变体是由Parys(2019)以及Lehtinen,Schewe和Wojtczak(2019)提出的。研究和利用的中心概念是吸引子分解的dominia在奇偶游戏和有序树描述的诱导结构的吸引子分解。通用算法产生McNaughton-Zielonka,Parys和Lehtinen-Schewe-Wojtczak算法作为特殊情况下,适当的通用树作为输入。主要的技术成果提供了一个统一的证明的正确性和结构的见解,这些算法。将奇偶对策的通用算法适当地应用于不动点对策,给出了有限完备格上计算嵌套不动点的拟多项式时间算法。奇偶对策和嵌套不动点的通用算法可以符号化实现。它展示了如何使用$O(\lg d)$符号空间复杂度来实现这一点,改进了Chatterjee,Dvotelák,Henzinger和Svozil(2018)为奇偶游戏实现的$O(d \lg n)$符号空间复杂度,其中$n$是顶点的数量,$d$是奇偶游戏中不同优先级的数量。
2022-08-29 cs.DS cs.FL cs.GT
Alternating Traps in Muller and Parity Games
穆勒游戏是由两个玩家沿着图移动一个令牌进行的;获胜者由出现频率无限高的顶点集决定。算法的核心问题是为玩家计算获胜区域。不同的类和表示的穆勒游戏导致不同的计算复杂性的问题。其中一类是奇偶校验游戏,这些是特别重要的计算复杂性,因为他们仍然是少数组合问题之一,已知在NP和合作NP,但不知道是在P.我们表明,获胜的地区穆勒游戏可以确定其陷阱的交替结构。然后,我们将一个自然数与每一个穆勒博弈联系起来,我们称之为陷阱深度;这个参数衡量陷阱结构的复杂程度。我们提出了算法的奇偶校验游戏运行在多项式时间的图形有界陷阱深度,并在一般情况下运行在时间指数的陷阱深度。
2013-07-23 cs.DS cs.GT cs.LO
Time and Parallelizability Results for Parity Games with Bounded Tree and DAG Width
奇偶博弈是NP相交CoNP中的一类研究较多的博弈,这些博弈在P中并不存在。因此,研究人员考虑了某些图形参数较小的情况下的专门算法。本文研究了树宽有界的图和DAG宽度有界的图上的奇偶对策。我们证明了有界DAG宽度的奇偶博弈可以在O(n^(k+3)k^(k + 2)(d + 1)^(3 k + 2))时间内求解,其中n,k和d是奇偶博弈的大小,树宽和优先级数量。这是对Berwanger等人给出的先前最佳算法的改进,时间复杂度为n^O(k^2)。我们还证明了,如果提供一个树分解,那么有界树宽的奇偶博弈可以在O(nk ^(k + 5)(d + 1)^(3 k + 5))时间内解决。这比Obdrzalek给出的以前最好的算法有所改进,该算法运行时间为O(n d^(2(k+1)^2))。我们的技术也可以用来证明解决具有有限树宽的奇偶博弈的问题属于复杂性类NC^2,这是一类可以有效并行化的问题。这与一般的奇偶博弈问题形成鲜明对比,后者被认为是P-困难的,因此不太可能包含在NC中。
2013-06-17 cs.GT
Graph Searching, Parity Games and Imperfect Information
我们研究了图搜索博弈和不完全信息博弈之间的相互关系。作为关键的结果,我们得到了有界不完美信息的奇偶博弈可以解决在PTIME上的有界DAG-宽度的图,推广了奇偶博弈的几个结果有界复杂性的图。我们使用了一种新的图搜索概念,几个警察试图抓住多个劫匪,而不仅仅是一个劫匪。主要的技术结果是,单调地抓住r个强盗所需的警察数量至多是图的DAG宽度的r倍。我们还探讨了这一新概念的各个方面,作为一个细化的有向路径宽度,强调其连接的概念,不完美的信息。
2011-10-25 cs.GT
A short proof of correctness of the quasi-polynomial time algorithm for parity games
最近,克里斯蒂安·S。Calude,Sanjay Jain,Bakhadyr Khoussainov,Wei Li和Frank Stephan提出了一个求解奇偶对策的拟多项式时间算法。本文提出了一个简短的证明他们的算法的正确性。
2017-04-24 cs.FL cs.GT
Parity and Streett Games with Costs
我们认为两个玩家的游戏有限图配备成本的边缘,并引入两个获胜的条件,成本平价和成本Streett,这需要的界限之间的成本请求和他们的反应。这两个条件推广了相应的经典ω-正则条件和相应的有限性条件。对于有成本的平价博弈,我们证明了第一个玩家有位置获胜策略,并且决定获胜者的策略取决于NP和coNP。对于Streett游戏的成本,我们表明,第一个球员有有限状态的获胜策略,并确定赢家是EXPTIME完成。第二个玩家可能在两个游戏中都需要无限的内存。这两种类型的博弈都可以通过线性求解其经典变体的许多实例来解决。
2014-06-24 cs.CC cs.GT cs.LO
A Super-Polynomial Lower Bound for the Parity Game Strategy Improvement Algorithm as We Know it
本文给出了Voege和Jurdziski提出的求解奇偶对策的离散策略改进算法的一个新的下界。首先,我们非正式地显示哪些结构是难以解决的算法。其次,我们概述了一个家庭的游戏的二次规模的算法需要指数级的许多战略迭代,回答在否定的长期存在的问题,该算法是否运行在多项式时间。此外,我们注意到,同一系列的游戏可以用来证明类似的结果w.r.t. Schewe的策略改进变体。
2009-01-18 cs.GT
Resource-Aware Automata and Games for Optimal Synthesis
我们考虑定量的奇偶自动机和奇偶游戏的概念,旨在模拟资源感知行为,并研究(内存满)策略展示接受运行,需要最小量的初始资源,分别为赢得一个游戏,最小的初始资源。我们还展示了这样的策略可以被简化为只包括两种类型的移动:前者旨在增加资源,后者旨在满足接受条件。
2019-09-17 cs.GT cs.LO
The complexity of solving reachability games using value and strategy iteration
近似求解两人零和并发可达对策的两个标准算法是值迭代和策略迭代。我们证明了2^(m^(Theta(N)的上界和下界的最坏情况下的迭代次数所需的这两个算法提供非平凡的近似值的游戏与N个非终端的位置和m个行动,每个球员在每个位置。特别是,这两种算法都具有双指数复杂度。即使作为输入的游戏只有一个非终端的位置,我们证明了一个指数下界的最坏情况下的迭代次数需要提供非平凡的近似。
2012-03-01 cs.GT
A Direct Reduction from Stochastic Parity Games to Simple Stochastic Games
本文提出一种从随机奇偶博弈到简单随机博弈的直接多项式时间归约,通过小工具变换移除优先级函数,证明了归约正确性并印证了SPGs的NP∩coNP复杂度。
2025-06-06 cs.GT
Attractors Is All You Need: Parity Games In Polynomial Time
Eindhoven University of Technology(埃因霍温理工大学)
本文提出一种仅移除已确定获胜者区域的新型吸引子算法,以多项式时间求解奇偶博弈并保证找到最小统治域,终结了该问题数十年的研究探索。
2025-11-04 cs.CC cs.DS cs.FL
Predicting Winning Regions in Parity Games via Graph Neural Networks (Extended Abstract)
German Aerospace Center (DLR)(德国航空航天中心(DLR));University of Stuttgart(斯图加特大学)
针对奇偶博弈求解缺乏多项式最坏情况复杂度算法的问题,提出一种基于图神经网络的不完备多项式时间方法来确定获胜区域,在900个随机生成的博弈上验证了其有效性与高效性。
2023-07-27 cs.GT cs.LG
Parity Games, Imperfect Information and Structural Complexity
我们解决的问题,解决不完美信息的有限图的结构复杂性有限的奇偶游戏。在PTIME中是否能解决完全信息的奇偶博弈是一个重要的开放问题。然而,限制游戏竞技场的结构复杂性通常会导致奇偶游戏的有效算法。这样的结果是已知的有界树宽度,DAG宽度,有向路径宽度,纠缠,我们描述的警察和强盗游戏的图形类。相反,不完美信息的引入使问题变得更加困难,它变得EXPTIME困难。我们分析了这两种方法的相互作用。我们用一个简单的方法来衡量一个玩家的“无意识”量,即不完美信息的量。事实证明,如果它是无界的,低结构复杂度并不能使问题更简单。即使在非常简单的图上,它仍然是EXPTIME-硬的或PSPACE-硬的。对于有界不完美信息的游戏,我们分析了幂集结构,这是常用的不完美信息的游戏转换成一个等价的游戏与完美的信息。这种构造保持了有向路径宽度和DAG宽度的有界性,但不保持纠缠和树宽度的有界性。因此,如果有向路径宽度或DAG宽度是有界的,则具有有界不完美信息的奇偶博弈可以在PTIME中求解。对于DAG宽度,我们遵循两种方法。一个导致一个已知的事实,即完美的信息奇偶性游戏是在PTIME,如果DAG宽度是有界的推广。我们证明了这个定理的非单调DAG宽度。另一种方法是在有向图上引入一个警察和强盗的游戏(有多个强盗),被认为是Richerby和Thilikos的无向图。我们证明了一个严格的线性约束的数量需要额外的警察抓住一个…
2017-03-02 cs.GT
Robustness of Structurally Equivalent Concurrent Parity Games
我们考虑在有限状态空间上进行无限回合的两人随机博弈。游戏是并行的:在每一轮中,两个参与者(参与者1和参与者2)独立地并且同时地选择他们的移动;当前状态和两个移动确定在后继状态上的概率分布。我们还考虑了回合制随机游戏的重要特例,玩家轮流移动,而不是同时移动。我们研究了以ω-正则获胜条件为奇偶目标的并发博弈。参与人1的奇偶目标值是参与人能够保证满足对手所有策略的目标的最大概率。研究了在转移概率不精确的情况下,并发和回合制随机奇偶博弈中价值函数的连续性和鲁棒性问题。我们提出的价值函数的差异(在转移概率的不精确性方面)的定量界限,并显示了结构上等价的并发游戏(两个游戏是结构上等价的,如果支持的转移函数是相同的,概率不同)的价值连续性。我们还证明了结构等价的回合制随机奇偶博弈的最优策略的鲁棒性。最后,我们表明,价值连续性属性打破结构上等价的假设(即使是马尔可夫链),并表明我们的定量界是渐近最优的。因此,我们的结果是紧的(假设是必要的和充分的)和最优的(我们的定量界是渐近最优的)。
2012-01-03 cs.GT
Solving Streett and Emerson-Lei Games with Universal Trees
University of Liverpool(利物浦大学);University Warwick(华威大学);University of Gothenburg(哥德堡大学);Chalmers University of Technology(查尔姆斯理工大学)
本研究阐释通用树与Zielonka树在Streett、Emerson-Lei博弈求解中的作用,改进其复杂度,生成内存最优策略,并优化Zielonka-McNaughton算法的符号实现。
2026-08-18 cs.GT cs.LO
Graph Operations on Parity Games and Polynomial-Time Algorithms
奇偶游戏是在有向图上进行的游戏,其顶点由自然数标记,称为优先级。玩家沿着有向图的边缘推一个记号。获胜者是由在这个无限博弈中无限频繁出现的最大优先权的对等决定的。研究奇偶博弈的一个动机来自于通过模型检验对系统进行形式化验证的领域。在奇偶博弈中决定赢家是多项式时间等价于模态μ演算的模型检验问题。另一个强大的动机在于,解决奇偶博弈的精确复杂性是一个长期存在的开放问题,目前最知名的算法是次指数。已知问题是在复杂性类UP和coUP中。在本文中,我们确定了限制类的有向图的问题是可解的多项式时间,从结构图理论的方法。我们考虑三个标准的图形操作:两个图的连接,沿着顶点重复粘贴,以及添加一个顶点。给定一类C的有向图,我们可以解决奇偶游戏在多项式时间,我们表明,同样适用于从C获得的类,通过应用一次这三个操作的任何一个元素。这些结果提供,特别是,多项式时间算法的奇偶校验游戏的基础图是一个方向的完全图,完全二分图,块图,或块仙人掌图。这些类的问题是不知道是有效的解决。关于限制类的奇偶对策是在多项式时间可解的先前的结果包括类的有界树宽度,有界DAG宽度,和有界树宽度。我们还证明,承认一个平价游戏的获胜区域并不比从头开始计算它们更容易。
2012-08-08 cs.CC cs.GT
The Strahler number of a parity game
根树的Strahler数是完美二叉树的最大高度,它是它的子树。提出了奇偶对策的Strahler数定义为任意吸引子分解的树的最小Strahler数。证明了奇偶对策在拟线性空间和时间上都是可解的,即关于点数$n$是多项式的,关于$({d}/{2k})^k$是线性的,其中$d$是优先数,$k$是Strahler数.这种复杂性是准多项式的,因为Strahler数最多是顶点数的对数。证明是基于一个新的建设小Strahler通用树。证明了奇偶对策的Strahler数是一个鲁棒参数:它与基于进度测度树的替代版本和Lehtinen~(2018)定义的寄存器数一致。由此得出奇偶对策可以在准线性空间和时间中求解,即在$({d}/{2k})^k$中顶点数是多项式且线性的,其中$k$是寄存器号。这显着提高了Lehtinen(2018)和Parys(2020)对有界寄存器数奇偶博弈的运行时间和空间。基于小Strahler泛树的算法的运行时间产生了一个新的权衡$k \cdot \lg(d/k) = O(\log n)$之间的两个自然参数,测量的结构复杂性的奇偶游戏,这使得解决奇偶游戏在多项式时间。这包括Calude、Jain Khoussainov、Li和Stephan(2017)、Jurdzienski和Lazić(2017)以及Lehtinen(2018)的结果所涵盖的参数的渐近设置作为特殊情况,并且它显…
2020-05-04 cs.DS cs.FL cs.GT
Universal trees grow inside separating automata: Quasi-polynomial lower bounds for parity games
自从Calude,Jain,Khoussainov,Li和Stephan(2017)的突破性结果以来,已经提出了几种不同的技术来设计用于解决奇偶游戏的准多项式算法:游戏摘要,进度测量和注册游戏。我们认为,所有这些技术都可以被视为实例的分离方法来解决平价游戏,其中一个关键的技术组成部分是构建(显式或隐式)的自动机,分离语言的文字编码播放(决定性地)赢得了两个球员。我们的主要技术成果是一个准多项式下界的大小,这样的分离自动机,几乎匹配目前最好的上限。这就形成了一个障碍,所有现有的方法必须克服正在进行的寻求多项式时间算法解决奇偶博弈。我们引入和研究的关键和基本概念是泛序树。技术亮点是泛有序树的大小的准多项式下界和证明每个分离安全自动机有一个泛树隐藏在其状态空间。
2018-11-02 cs.CC cs.FL cs.GT