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的猜测是简单的对照人的构成封闭的估算，我们将构造不需要的估算，我们将构造不需要的工具，以构造不需要的工具，以构造自己的构造技术。我们将确定结构性估值的哪些属性可以保证运行策略改进算法的可能性，这些算法为解决无限持续时间游戏提供了有效且实用的解决方案。将我们的特征专门针对平等游戏，我们将设计新的可扩展策略改进框架（具有准多项式最差的运行时间），或者给出正式的证据表明这种结构不存在。