Below the Branches of Universal Trees

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

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.