Below the Branches of Universal Trees

解决奇偶性游戏是一个有趣的问题，它结合了实际意义和长期存在的学术挑战。它的实际意义来自于它作为安全关键系统的自动构造（综合）和证明正确性（模型检查）中最困难和最昂贵的步骤的首要地位。它在嵌套不动点的求值和热带代数中有进一步的应用。这在学术上很有趣，因为解决奇偶性游戏的复杂性是一个长期存在的挑战。对解决奇偶对策的计算复杂性的理论理解是一个令人垂涎的奖项，因为有效解决奇偶对策的算法挑战首次出现在20世纪90年代初，是一个基本而有影响力的开放问题。例如，多项式时间算法的存在性最近被列为ACM SIGLOG新闻的自动机专栏中六个最重要的开放问题之一。这个高风险的项目将试图证明解决奇偶性博弈的计算成本很低。尝试这一挑战是大胆的（就像新视野项目应该做的那样），但它也很及时：五年前所有的算法都是指数型的，而最近已经建立了许多不同的方法，它们仅仅是准多项式。这使得第一次尝试打破多项式时间的最后障碍，从而实现有效的算法。项目在科学好奇心的驱动下，也为后续研究提供了更高的技术准备水平的传送带：一旦原则上建立了可处理的算法，高效的算法就会随之而来，它们将有助于创建更快的模型检查和合成工具，最终有助于更安全，更好的软件。

Solving parity games is an intriguing problem that combines practical relevance with a long standing academic challenge. Its practical relevance is drawn from its prime position as the most difficult and most expensive step in automatically constructing (synthesis) and proving the correctness (model checking) of safety critical systems. It has further applications in the evaluation of nested fixed points and tropical algebra.It is academically intriguing, because the complexity of solving parity games is a long standing challenge. The theoretical understanding of the computational complexity of solving parity games is a coveted prize since the algorithmic challenge of solving parity games efficiently first arose as a fundamental and impactful open problem posed in the early 1990s. For example, the existence of a polynomial-time algorithm has been recently listed as one of the six most important open problems in the Automata Column of the ACM SIGLOG News.This high-risk project will attempt to show that solving parity games is computationally cheap.Attempting this challenge is bold (as it should be for a New Horizons project), but it is also timely: while five years ago all algorithms were exponential, a number of different approaches that are merely quasi-polynomial have recently been established. This makes the attempt to tear down the last barrier to polynomial time, and thus to efficient algorithms, is within reach for the first time.While the project is driven by scientific curiosity, it also feeds the conveyor belt of achieving higher technology readiness levels in follow-up research: once tractable algorithms are established in principle, highly efficient algorithms follow in due course, and they will help creating faster model checking and synthesis tools, and ultimately contributing to safer and better software.