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.

解决平等游戏是一个有趣的问题，它将实际相关性与长期以来的学术挑战相结合。它的实际相关性是从其主要位置作为自动构建（合成）和证明安全关键系统的正确性（型号检查）的最困难和最昂贵的步骤的最佳地位。它在评估嵌套固定点和热带代数的评估中有进一步的应用。这在学术上很有趣，因为解决平等游戏的复杂性是一个长期的挑战。对解决平价游戏的计算复杂性的理论理解是一个令人垂涎的奖项，因为算法挑战有效地解决了平等游戏，这是1990年代初期提出的一个基本和有影响力的开放问题。 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最近已经建立了仅准多项式的。这使得拆除多项式时间的最后障碍，从而拆除有效的算法，这是第一次可以触及。尽管该项目是由科学的好奇心驱动的，但它还为实现后续研究中高级技术准备水平的传送带提供了良好的算法：一旦建立了且有效的算法，并且在算法上建立了较高的算法，并在此过程中建立了算法，并在此过程中建立了良好的算法。并最终为更安全，更好的软件做出贡献。