COSTRA -- The Cost of Winning Strategies

我们研究计算的数学模型，这是理解和解释人工智能系统和其他计算机程序行为的必要前提。网络物理系统越来越多地影响我们生活的大多数方面：它们被用于起搏器、管理工厂供应链、股票交易以及自动驾驶现代飞机和汽车。软件缺陷可能会产生严重的经济和危及生命的后果。虽然传统的测试和模拟方法可以有效地发现错误，但它们无法显示错误的缺失。一种更有希望的方法是使用数学论证来证明系统在所有可能的情况下都能按预期运行。验证是基于这一思想的研究领域。它是真正的跨学科，与人工智能、离散数学和软件工程有着令人着迷的联系。为了证明某个系统的正确性，人们首先要从系统本身的正式模型以及定义正确性含义的规范开始。例如，在模型检测中，我们将系统建模为有限状态机，将规范建模为时态逻辑公式。然后，正确性取决于有限状态机满足公式的事实，该公式通常可以被自动验证。当然，有许多不同的方法来形式化系统和规范，一些形式化比另一些更具表现力。目前的方法非常擅长分析只有有限多个内部配置的模型，如微芯片或硬件驱动程序。然而，如果我们转向更具表现力的模型，我们很快就会超出已知技术的范围，甚至跨越理论界限。在这一点上，研究前沿是所谓的无限状态模型，它使我们能够直接争论诸如实时约束、递归深度或同时的用户请求等无界量。例如，假设一个网络服务器可以并发地接收任意数量的请求，并且最终应该响应所有请求。请求的总数不是预先确定的，因此有必要将其合并到模型中，因此模型具有无限多个可能的内部配置。然而，我们确实有很好的有限表示，例如计数器机器或下推自动机，可以在这种情况下使用。其结果是在这些形式主义的可表现性和它们的验证的可行性之间进行权衡。在存在环境不确定性的情况下，正确性检查和决策的关键数学工具是敌对参与者之间的博弈，他们分别试图造成错误和防止错误。在经济学、生物学、化学和其他科学中，密切相关的形式主义以马尔可夫链和马尔可夫决策过程的形式使用。这里的正确性对应于获胜策略的存在，这些策略告诉他们的玩家如何移动以确保胜利。制胜策略很重要，不仅因为它们充当正确性证书，还因为它们通常可以直接转换为可执行代码。我们的研究试图了解更一般的无限策略，这通常是现实规范所必需的。我们将调查数学结构、内部复杂性，从而研究制胜策略的成本。提高我们对策略的理解有望产生更好的有限表示，这反过来使验证获胜策略的存在(检查正确性)以及自动生成和执行获胜策略变得更容易。我们的研究使我们对计算和决策的本质有了更深的理解，并为自动化程序验证提供了新的和改进的方法。

We investigate mathematical models of computation, which is a necessary precondition to understand and explain the behaviour of AI systems and other computer programs.Cyber-physical systems increasingly affect most aspects of our lives: they are used in pacemakers, manage factory supply chains, trade in stocks and autonomously pilot modern planes and cars. Software deficiencies can have serious economic and life-threatening consequences. While traditional methods of testing and simulations can be effective for finding errors, they are hopelessly inadequate for showing their absence. A more promising approach is to use mathematical arguments to prove that a system behaves as intended, in all possible situations. Verification is the area of research based on this idea. It is truly interdisciplinary and has fascinating connections to Artificial Intelligence, Discrete Mathematics and Software Engineering.To prove the correctness of some system one starts with a formal model of the system itself as well as a specification that defines what correctness means. In model-checking, for instance, we model systems as a finite-state machine and the specifications as temporal logic formulae. Correctness then ammounts to the fact that the finite-state machine satisfies the formula, which can often be verified automatically. Naturally, there are many different ways to formalize systems and specifications, and some formalisms are more expressive than others.Current methods are very good at analysing models with only finitely many internal configurations, such as microchips or hardware drivers. However, if we move to more expressive models we quickly go beyond the reach of known techniques or even cross theoretical limits. At this point the research frontier is on so-called infinite-state models, which enable us to argue directly about unbounded quantities such as realtime constraints, recursion depth or simultaneous user requests.For example, imagine a network server that can receive any number of requests concurrently and which should eventually respond to all of them. The total number of requests is not determined in advance and so it is necessary to incorporate it into the model, which consequently has infinitely many possible internal configurations. However, we do have good finite representations, such as Counter Machines or Pushdown Automata, that can be used in such situations. The result is a trade-off between the expressibility of these formalisms and the feasibility of their verification.A key mathematical tool for correctness checks and decision making in the presence of environmental uncertainty are games between antagonistic players, who try to cause and prevent errors, respectively. Closely related formalisms are used in Economics, Biology, Chemistry and other sciences, in the form of Markov Chains and Markov Decision Processes.Correctness here corresponds to the existence of winning strategies, which tell their player how to move in order to secure a win. Winning strategies are important not only because they act as correctness certificates but also because they can often be directly translated into executable code.Our research seeks to understand more general, infinitary strategies, which are often necessary for realistic specifications. We will investigate the mathematical structure, internal complexity, and thus the cost of winning strategies. Advancing our understanding of strategies promises to yield better finite representations, which in turn makes it easier to verify that winning strategies exist (checking correctness) as well as automatically generating and executing them.Our research leads to a deeper understanding of the nature of computation and decision making and provides new and improved methods for automated program verification.