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 News的Automata专栏列为六个最重要的开放问题之一，这个高风险的项目将试图表明解决奇偶博弈在计算上是廉价的，尝试这一挑战是大胆的（就像新视野项目一样），但它也很及时：虽然五年前所有的算法都是指数的，但是最近已经建立了许多仅仅是准多项式的不同方法。这使得试图拆除多项式时间的最后一个障碍，从而有效的算法，是触手可及的第一次。虽然该项目是由科学的好奇心驱动，它也饲料输送带实现更高的技术准备水平在后续研究：一旦在原则上建立了易处理的算法，高效的算法将在适当的时候出现，它们将有助于创建更快的模型检查和综合工具，并最终有助于更安全和更好的软件。

项目成果

Automated Technology for Verification and Analysis - 21st International Symposium, ATVA 2023, Singapore, October 24-27, 2023, Proceedings, Part I

验证和分析自动化技术 - 第 21 届国际研讨会，ATVA 2023，新加坡，2023 年 10 月 24-27 日，会议记录，第一部分

• DOI: 10.1007/978-3-031-45329-8_3
• 发表时间: 2023
• 作者: Li Y

Semantic Flowers for Good-for-Games and Deterministic Automata

适用于游戏和确定性自动机的语义花

• DOI: 10.1016/j.ipl.2023.106468
• 发表时间: 2023
• 期刊: Information Processing Letters
• 影响因子: 0.5
• 作者: Dell'Erba D

ECAI 2023 - 26th European Conference on Artificial Intelligence, September 30-October 4, 2023, Kraków, Poland - Including 12th Conference on Prestigious Applications of Intelligent Systems (PAIS 2023)

ECAI 2023 - 第 26 届欧洲人工智能会议，2023 年 9 月 30 日至 10 月 4 日，波兰克拉科夫 - 包括第 12 届智能系统著名应用会议 (PAIS 2023)

• DOI: 10.3233/faia230499
• 发表时间: 2023
• 作者: Salimi P

An Objective Improvement Approach to Solving Discounted Payoff Games

解决折扣支付游戏的客观改进方法

• DOI: 10.4204/eptcs.390.13
• 发表时间: 2023
• 期刊: Electronic Proceedings in Theoretical Computer Science
• 作者: Dell'Erba D