COSTRA -- The Cost of Winning Strategies

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

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.