Verification of Linear Dynamical Systems

点击翻译按钮获取中文摘要

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.