Verification of Linear Dynamical Systems

自动化验证领域关注的是建立和分析计算机系统的数学模型，以确保其可靠性和可靠性。理想情况下，这些模型应该在系统构建之前就被用来分析系统。通常，模型不仅包括系统，还包括其环境，从而导致包括物理和计算过程的复杂行为。线性动力系统是一种自然的模型，它在从控制工程到经济学和理论生物学的定量科学中得到了广泛的研究。在自动验证中，线性动态系统作为简单计算机程序的模型出现，例如，一段代码中的循环，它对程序变量进行线性更新，或者是控制与控制软件交互的物理过程行为的线性微分方程。虽然从其他科学的角度来看，线性动力系统可能被认为是相对简单的，自动验证所需的那种精确和详尽的分析带来了相当大的挑战，该领域充满了自然的开放问题。一个突出的例子涉及决定简单线性循环的终止，也就是说，非常简单的程序没有条件，只对它们的变量进行线性赋值。虽然这样的程序太简单了，不能单独使用，但当它们描述更复杂的循环的行为时，它们形成了自然的抽象。许多注意力已经支付给证明终止这样的程序和许多强大的方法已经开发出来，但作为yetno通用程序是已知的，是保证告诉是否给定的简单线性循环将终止。这种情况被著名的理论计算机科学家理查德·利普顿（Richard Lipton）描述为“数学上的尴尬”，而数学家泰伦斯·陶（Terrence Tao）则评论说：“这是说，我们甚至不知道如何决定线性自动机的停机问题。“.这个项目的目标是发展技术，以有助于自动核查的方式分析线性动力系统，例如，确定其行为由微分方程决定的系统变量是否能够进入临界状态。该项目的主要挑战是，尽管系统的短期行为很简单，但系统的长期演变分析起来可能非常复杂。该项目考虑了不同类型系统的一系列验证问题，包括离散时间和连续时间系统。该项目的方法的一个重要组成部分来自丢番图逼近的主题，这是数论中的一个经典主题，与遍历理论和动力系统有着天然的联系。

The field of automated verification concerns itself with building and analysing mathematical models of computer systems in order to ensure their dependability and reliability. Ideally suchmodels should be used to analyse a system before it is built. Often the models include not just the system, but also its environment, leading to complex behaviours which include both physical and computational processes. A natural class of models for this task are linear dynamical systems, which are widely studied across the quantitative sciences, from control engineering to economics and theoretical biology. Within automated verification, linear dynamical systems arise as models of simple computer programs, e.g., a loop in a piece of code which makes linear updates to program variables, or a linear differential equation governing the behaviour of physical processes that are interacting with control software. Although from the point of view of other sciences linear dynamical systems might be considered relatively simple, the kind of precise and exhaustive analyses required in automated verification pose considerable challenges, and the area is rich with natural open problems. A striking example concerns deciding the termination of simple linear loops, that is, very simple while programs with no conditionals that only make linear assignments to their variables. Although such programs are too simple to be of much use on their own, they form natural abstractions when consideringthe behaviour of more complex loops. Much attention has been paid to proving termination of such programs and many powerful methods have been developed, but as of yetno general purpose procedure is known that is guaranteed to tell whether or not a given simple linear loop will terminate. This situation has been described as by Richard Lipton, a leading theoretical computer scientist, as a "mathematical embarrassment", while the mathematician Terrence Tao remarks that "it is saying that we do not know how to decide the halting problem even for linear automata!".The goal of this project is to develop techniques to analyse linear dynamical systems in the kind of terms that are useful automated verification, for example, to determine whether asystem variable whose behaviour is determined by differential equation can ever enter a critical state. The main challenge in the project is that the long-term evolution of systems can be verycomplex to analyse even though their short-term behaviour is simple. The project considers a range of verification problems for different types systems, including discrete-time and continuous-time systems. An important component of the methodology of the project comes from the subject of Diophantine approximation, a classical topic in number theory, with natural connections to ergodic theory and dynamical systems.