Valuation Structures for 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.