Verification of Linear Dynamical Systems

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

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.