Valuation Structures for Infinite Duration Games

无限期游戏的估值结构

• 批准号: EP/Y027663/1
• 负责人: Sven Schewe
• 金额: $ 25.55万
• 依托单位: University of Liverpool
• 依托单位国家: 英国
• 项目类别: Fellowship
• 财政年份: 2023
• 资助国家: 英国
• 起止时间: 2023 至 无数据
• 项目状态: 未结题
• 来源: https://gtr.ukri.org/projects?ref=EP%2FY027663%2F1
• 关键词: Valuation; Structures; Infinite; Duration; Games

Infinite duration games are the natural and elegant mathematical model underlying reactive systems: non-terminating systems that maintain a continuous interaction with their environment. Hardware circuits, communication protocols, and embedded controllers are typical examples. The unicorn for these systems is reactive synthesis: an approach that takes automatically construct reactive controllers directly from a given specification (or proves that no such controller exists). The need for designing increasingly complex synthesis scenarios motivates the study of infinite duration games, which have attracted considerable attention in the past twenty years or so.A recent progress has been achieved by the introduction of structured valuations, a new and powerful tool in the study of infinite duration games. Structured valuations are quantitative specifications induced by a graph structure with further monotonicity requirements. We will capture well-studied specifications using structured valuations that will allow us to uniformly analyse and manipulate them. We will tackle ambitious structural (how complex are controllers implementing a given specification) as well as algorithmic (how to decide existence of such a controller) questions for infinite duration games through the lens of structured valuations.We will prove Kopczynski's conjecture that specifications that admit simple controllers are closed under unions, we will design techniques to construct structured valuations that capture unions of general classes of specifications. We will determine which properties of structured valuations guarantee the possibility of running strategy improvement algorithms, which provide efficient and practical solutions for solving infinite duration games. Specialising our characterisation to parity games, we will either design new scalable strategy improvement frameworks (with quasi-polynomial worst-case running time) or give formal evidence that such structures do not exist.

无限持续时间游戏是反应系统的自然和优雅的数学模型：与环境保持持续交互的非终止系统。硬件电路、通信协议和嵌入式控制器是典型的例子。这些系统的独角兽是反应式合成：一种直接从给定规范自动构建反应式控制器（或证明不存在这样的控制器）的方法。无限久期博弈的研究在近二十年来受到了广泛的关注，结构化估值方法是研究无限久期博弈的一个新的有力工具。结构化估值是由具有进一步单调性要求的图结构引起的定量规范。我们将使用结构化估值来捕捉经过充分研究的规格，这将使我们能够统一分析和操纵它们。我们将解决雄心勃勃的结构性问题，（控制器实现给定规范的复杂程度）以及算法（如何判定这样一个控制器的存在性）问题的无限持续时间的游戏通过透镜的结构估值。我们将证明Kopczynski的猜想，规范，承认简单的控制器是封闭的工会，我们将设计技术来构建结构化的估值，以捕获一般类别的规范的联合。我们将确定结构化估值的哪些属性保证了运行策略改进算法的可能性，这些算法为解决无限持续时间游戏提供了有效和实用的解决方案。专门我们的特点，平价游戏，我们将设计新的可扩展的战略改进框架（准多项式最坏情况下的运行时间）或正式的证据表明，这种结构不存在。