Valuation Structures for Infinite Duration Games

无限持续时间的游戏是反应性系统的自然而优雅的数学模型：维持与环境持续互动的非终止系统。硬件电路、通信协议和嵌入式控制器是典型的例子。这些系统的独角兽是反应性合成：一种直接从给定规范（或证明不存在这样的控制器）自动构造反应性控制器的方法。设计越来越复杂的综合场景的需求推动了对无限持续时间游戏的研究，这在过去20年左右的时间里引起了相当大的关注。最近的一个进展是引入了结构化估值，这是研究无限持续博弈的一种新的强大工具。结构化估值是由具有进一步单调性要求的图结构引起的定量规范。我们将使用结构化估值来获取经过充分研究的规范，这将允许我们统一地分析和操作它们。我们将通过结构化估值的视角来解决无限持续时间游戏的结构性问题（控制器执行给定规范的复杂程度）和算法问题（如何决定这样一个控制器的存在）。我们将证明Kopczynski的猜想，即承认简单控制器的规范在联合下是封闭的，我们将设计技术来构建结构化估值，以捕获规范的一般类的联合。我们将确定结构化估值的哪些属性保证了运行策略改进算法的可能性，这些算法为解决无限持续博弈提供了有效和实用的解决方案。将我们的特征专一化到奇偶性游戏，我们要么设计新的可扩展策略改进框架（带有拟多项式最坏情况运行时间），要么给出这种结构不存在的正式证据。

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.