Below the Branches of Universal Trees

普世树枝下

基本信息

批准号：
EP/X017796/1
负责人：
Sven Schewe
金额：
$ 25.76万
依托单位：
University of Liverpool
依托单位国家：
英国
项目类别：
Research Grant
财政年份：
2023
资助国家：
英国
起止时间：
2023 至无数据
项目状态：
未结题

来源：
https://gtr.ukri.org/projects?ref=EP%2FX017796%2F1
关键词：
Below Branches Universal Trees

项目摘要

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.

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