From Local To Global Optimality in Concurrent Parity Games
本文研究了有限图上的双人并发随机奇偶博弈，提出了一个在每个状态满足时即可保证双方玩家均存在位置最优策略的局部结构条件。
2023-11-24 cs.GT
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
Energy Parity Games
能量平价游戏是在加权图上进行的无限两人回合制游戏。游戏的目标结合了（定性）奇偶条件和（定量）要求，即权重之和（即，游戏中的能量水平）必须保持积极。除了他们自己的兴趣在设计和合成的资源受限的ω-正规规格，能量平价游戏提供了一个最简单的模型，结合定性和定量的目标。我们的主要结果如下：（a）指数记忆对于能量奇偶博弈中的获胜策略是必要的和充分的;（b）能量奇偶博弈中的获胜者决定问题可以在NP \cap coNP中解决;（c）我们给出了一个通过还原为能量博弈来求解能量奇偶的算法.我们还表明，在能量平价游戏中决定赢家的问题是多项式等价的平均收益平价游戏中决定赢家的问题，而最佳策略可能需要无限的内存在平均收益平价游戏。因此，我们得到了一个概念上简单的算法来解决平均支付平价游戏。
2012-04-03 cs.GT cs.LO
A reduction from parity games to simple stochastic games
图上的博弈为反应式非终止系统提供了一个自然的模型。在这样的游戏中，两个玩家在竞技场上的交互导致描述系统运行的无限路径。在计算机科学中，不同的设置被用来对各种开放系统进行建模，例如基于回合或并发的移动，以及确定性或随机性的转换。在本文中，我们感兴趣的回合制游戏，特别是在确定性奇偶游戏和随机可达性游戏（也称为简单随机游戏）。我们提出了一个简单的，直接的和有效的减少从确定性奇偶游戏简单的随机游戏：它产生一个舞台的大小是线性的对数因子的原始舞台的大小。
2011-06-07 cs.GT
Memoryless Determinacy of Infinite Parity Games: Another Simple Proof
1998年，Zielonka简化了无限奇偶博弈的无记忆确定性的证明。在2018年，哈达德简化了有限奇偶博弈的无记忆确定性的一些证明。本文将哈达德的技术应用于无限奇偶博弈。给出了两个证明，一个更短，一个更建设性的。他们都没有使用Zielonka的陷阱和吸引子。
2018-11-21 cs.GT cs.LO
The discrete strategy improvement algorithm for parity games and complexity measures for directed graphs
一段时间以来，Jurdzinski和Voge提出的离散策略改进算法被认为是解决多项式时间奇偶博弈的候选算法。然而，奥利弗·弗里德曼最近证明了策略改进算法需要超多项式的许多迭代步骤，对于所有流行的局部改进规则，包括switch-all（也具有Fearnley的圈套记忆），switch-best，random-facet，random-edge，switch-half，least-recently-considered和Zadeh的Pivoting规则。我们分析了弗里德曼提供的例子中的复杂性措施的有向图，如树宽，DAG宽度，凯利宽度，纠缠，有向路径宽度，和cyclop宽度。我们知道，对于每一类奇偶博弈，只要其中一个参数是有界的，就可以有效地计算出获胜区域。事实证明，对于几乎所有这些措施，弗里德曼的反例的复杂性是有界的，实际上在大多数情况下，由非常小的数字。这种分析在某种意义上加强了弗里德曼的结果，并表明离散策略改进算法甚至比人们想象的更有限。它不仅需要超多项式的运行时间在一般情况下，多项式时间的可解性的问题是开放的，它甚至有超多项式的时间下限自然类的奇偶游戏上的有效算法是已知的。
2012-10-09 cs.CC cs.GT
Local Strategy Improvement for Parity Game Solving
奇偶博弈的求解问题是模型检验、可满足性检测和程序合成中许多问题的核心。解决奇偶博弈的一些最好的算法是策略改进算法。这些都是全球性的，因为它们需要整个平价博弈在一开始就存在。这是一个明显的缺点，因为在许多应用中，人们只需要知道特定节点属于哪个获胜区域，并且见证获胜策略可能只覆盖整个游戏图的一小部分。我们提出了一个局部策略改进算法，该算法在执行改进步骤的同时探索游戏图。我们还比较了它与现有的全局策略改进算法和目前唯一的其他局部算法解决奇偶博弈的经验。事实证明，局部策略改进可以超过其他策略几个数量级。
2010-06-08 cs.CC cs.DS cs.GT
Parity Game Reductions
奇偶博弈在模型检验和可满足性检验中起着核心作用。求解奇偶性博弈在计算上是昂贵的，除其他外，由于博弈的大小，对于模型检验问题，其可以容易地包含$10^9$顶点或更多。等价关系可以用来减少奇偶博弈的规模，从而潜在地减轻部分计算负担。我们重新考虑（治理）互模拟和（治理）口吃互模拟，我们给出了详细的证明，这些关系是等价的，有唯一的等价物，他们近似的获胜地区的奇偶游戏。此外，我们提出了基于游戏的这些关系的特征。使用这些特征，我们的等价关系的奇偶游戏，可以在文献中找到，如直接模拟等价和延迟模拟等价。为了完成概述，我们开发的直接和延迟模拟等价的共归纳特征，我们建立了一个等价的奇偶游戏格。
2016-03-21 cs.GT cs.LO
Solving Parity Games on Integer Vectors
我们考虑无限图上的奇偶博弈，其中配置由控制状态和整数向量表示。这个框架包含了两个经典的博弈问题：状态向量加法系统上的奇偶博弈和多维能量奇偶博弈。我们证明了多维能量奇偶博弈问题是与vass上的单边奇偶博弈的一个子类可互约的，其中只有一个玩家可以修改整数计数器，对手只能改变控制状态。我们的主要结果是，这些单面奇偶对策的上闭获胜集的最小元素是可计算的。这意味着赢得多维能量平价博弈所需的最小初始信用的帕累托边界也是可计算的，解决了文献中的一个悬而未决的问题。此外，我们的主要结果暗示了有限状态系统与vass之间弱模拟前序/等价的可判定性，以及大片段模态μ演算的模型检验vass的可判定性。
2013-06-12 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
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
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
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
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
Benchmarks for Parity Games (extended version)
本文提出并在线发布了一个包含文献中所有奇偶博弈基准的测试套件，通过描述其生成方式和结构性质证明其代表性，为后续实验提供起点。
2015-01-16 cs.GT cs.LO
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
A Direct Reduction from Stochastic Parity Games to Simple Stochastic Games
本文提出一种从随机奇偶博弈到简单随机博弈的直接多项式时间归约，通过小工具变换移除优先级函数，证明了归约正确性并印证了SPGs的NP∩coNP复杂度。
2025-06-06 cs.GT
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
Attractors Is All You Need: Parity Games In Polynomial Time
Eindhoven University of Technology（埃因霍温理工大学）
本文提出一种仅移除已确定获胜者区域的新型吸引子算法，以多项式时间求解奇偶博弈并保证找到最小统治域，终结了该问题数十年的研究探索。
2025-11-04 cs.CC cs.DS cs.FL
Alpaga: A Tool for Solving Parity Games with Imperfect Information
Alpaga是一个求解不完全信息的两人平价博弈的算法。给定博弈的描述，它确定第一个参与者是否能确保获胜，如果是，它构造获胜策略。该工具提供了一个基于反链的最新算法的符号实现。
2009-01-29 cs.GT cs.LO
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
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
Robustness of Structurally Equivalent Concurrent Parity Games
我们考虑在有限状态空间上进行无限回合的两人随机博弈。游戏是并行的：在每一轮中，两个参与者（参与者1和参与者2）独立地并且同时地选择他们的移动;当前状态和两个移动确定在后继状态上的概率分布。我们还考虑了回合制随机游戏的重要特例，玩家轮流移动，而不是同时移动。我们研究了以ω-正则获胜条件为奇偶目标的并发博弈。参与人1的奇偶目标值是参与人能够保证满足对手所有策略的目标的最大概率。研究了在转移概率不精确的情况下，并发和回合制随机奇偶博弈中价值函数的连续性和鲁棒性问题。我们提出的价值函数的差异（在转移概率的不精确性方面）的定量界限，并显示了结构上等价的并发游戏（两个游戏是结构上等价的，如果支持的转移函数是相同的，概率不同）的价值连续性。我们还证明了结构等价的回合制随机奇偶博弈的最优策略的鲁棒性。最后，我们表明，价值连续性属性打破结构上等价的假设（即使是马尔可夫链），并表明我们的定量界是渐近最优的。因此，我们的结果是紧的（假设是必要的和充分的）和最优的（我们的定量界是渐近最优的）。
2012-01-03 cs.GT
Reachability Games and Parity Games
奇偶博弈是由位置决定的。这是一个基本的和经典的结果。2010年，Calude等人展示了有限奇偶博弈的突破性结果：获胜区域及其位置获胜策略可以在准多项式时间内计算。本文对这两个结果给出了完备的详细证明。本文中的结果并不意味着是原创的。位置的确定性结果显示可能无限的奇偶性游戏使用的想法Zielonka，他在1998年出版。为了展示准多项式时间，我们遵循Lehtinen在2018年介绍的寄存器游戏。虽然Lehtinen算法的时间复杂度不是最优的，但寄存器游戏本身在概念上是简单而有趣的。我们的各种证明要么是新的，要么是原始证明的简化。本文的主题包括可达对策的最优吸引子的定义和计算。
2022-08-22 cs.FL cs.GT cs.LO
Linear Complementarity Algorithms for Infinite Games
两个旋转算法的性能，由于Lemke和Cottle和Dantzig，研究线性互补问题（LCP）所产生的无限游戏，如奇偶校验，平均奖励，折扣游戏。该算法以前没有在无限博弈的背景下进行过研究，它们提供了经典策略改进算法的替代方案。这两个算法是纯粹的折扣游戏，从而绕过减少从游戏到LCP，从而促进更好地理解的算法时，应用于游戏。一个家庭的奇偶校验游戏，这两个算法在指数时间内运行，表明在最坏的情况下，他们没有更好的表现为奇偶校验，平均奖励，或折扣游戏比他们一般的P-矩阵LCP。
2009-09-30 cs.CC cs.DS cs.GT
Generating and Solving Symbolic Parity Games
我们提出了一个新的工具，验证模态μ演算公式的过程规范，基于符号奇偶游戏。它增强了现有的方法，首先编码的问题的参数化布尔方程系统（PBES），然后实例化PBES的奇偶性游戏。我们改进了从规范到PBES的转换以保持PBES中规范的结构，我们扩展了LTSmin以将PBES实例化为符号奇偶博弈，并实现了Zielonka的符号奇偶博弈递归求解算法。我们使用多值决策图（MDDs）来表示集合和关系，从而使工具能够处理非常大的系统。基于规范的结构划分转换关系，这允许有效地操纵MDD。我们进行了两个案例研究的模块化规范，表明新方法具有更好的时间和内存性能比现有的PBES为基础的工具，可以更快（但略低于内存效率）比符号模型检查NuSMV。
2014-07-30 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
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
A Recursive Approach to Solving Parity Games in Quasipolynomial Time
本文改进Zielonka经典递归算法，将奇偶博弈求解复杂度从指数级降至拟多项式级，达到$n^{O(\log(1+d/\log n))}$。
2022-01-11 cs.FL cs.GT
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
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
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
Solving Parity Games Using An Automata-Based Algorithm
奇偶博弈是一种抽象的无限轮博弈，在形式化验证中起着重要的作用。在基本设置中，这些游戏是两个玩家，回合制，并在有向图上的完美信息下进行，其节点标有优先级。游戏的赢家是根据在该游戏中无限频繁出现的最小优先级的奇偶性（偶数或奇数）来确定的。在奇偶博弈中找到一个获胜策略的问题是已知的，在UPTime $\cap$ CoUPTime和决定是否存在一个多项式时间的解决方案是一个长期存在的悬而未决的问题。在过去的二十年中，已经提出了各种算法。他们中的许多人也在一个名为PGSolver的平台上实现。这使得这些算法的经验评估和更好地了解他们的相对优点。在本文中，我们进一步促进这一主题的实施，第一次，交替自动机的基础上的算法。更确切地说，我们考虑一个算法介绍了Kupferman和Vardi，解决了一个奇偶性游戏解决相应的交替奇偶自动机的空性问题。我们的实证评估表明，该算法优于其他算法时，游戏有一个小数目的优先级相对于游戏的大小。在许多具体的应用中，我们确实会以优先级相对较少的奇偶博弈结束。这使得新算法在实践中非常有用。
2019-10-30 cs.DS cs.GT
Approximating the Value of Energy-Parity Objectives in Simple Stochastic Games
School of Informatics, University of Edinburgh（爱丁堡大学信息学院）
本文研究了简单随机游戏中能量-奇偶目标的近似计算问题，提出了一种在2-NEXPTIME内求解给定配置值的算法，并给出了玩家ε最优策略所需内存模式的上界。
2023-07-11 cs.GT math.PR
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
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
Time Flies When Looking out of the Window: Timed Games with Window Parity Objectives
窗口机制是由Chatterjee等人引入的，用于在图上的两人回合制游戏中加强具有时间界限的平均支付和总支付目标。从那以后，它被证明在各种环境中都很有用，包括游戏中的奇偶性目标和马尔可夫决策过程中的平均收益和奇偶性目标。我们研究时间自动机和定时游戏中的窗口奇偶性目标：给定窗口大小的界限，如果在路径上的所有状态中，我们看到一个足够小的窗口，其中最小的优先级是偶数，则路径满足这样的目标。我们发现，检查时间自动机的所有时间发散路径满足这样的窗口奇偶校验目标可以在多项式空间中完成，并且相应的时间游戏可以在指数时间内求解。这与计时奇偶游戏的复杂性相匹配，同时增加了推理时间界限的能力。我们还考虑了多维目标，并表明复杂性类不会增加。据我们所知，这是第一次在实时设置中研究窗口机制。
2021-08-11 cs.FL 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
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
Solving Odd-Fair Parity Games
本文研究Odd-fair parity games的高效求解，提出一种具有与Zielonka算法相同最坏时间复杂度的Zielonka型算法，并首次形式化了Odd玩家的获胜策略。
2023-10-23 cs.GT cs.SY eess.SY
Alternating Traps in Muller and Parity Games
穆勒游戏是由两个玩家沿着图移动一个令牌进行的;获胜者由出现频率无限高的顶点集决定。算法的核心问题是为玩家计算获胜区域。不同的类和表示的穆勒游戏导致不同的计算复杂性的问题。其中一类是奇偶校验游戏，这些是特别重要的计算复杂性，因为他们仍然是少数组合问题之一，已知在NP和合作NP，但不知道是在P.我们表明，获胜的地区穆勒游戏可以确定其陷阱的交替结构。然后，我们将一个自然数与每一个穆勒博弈联系起来，我们称之为陷阱深度;这个参数衡量陷阱结构的复杂程度。我们提出了算法的奇偶校验游戏运行在多项式时间的图形有界陷阱深度，并在一般情况下运行在时间指数的陷阱深度。
2013-07-23 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
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
