EPSRC Reference: 
EP/N008197/1 
Title: 
Verification of Linear Dynamical Systems 
Principal Investigator: 
Worrell, Professor JB 
Other Investigators: 

Researcher CoInvestigators: 

Project Partners: 

Department: 
Computer Science 
Organisation: 
University of Oxford 
Scheme: 
EPSRC Fellowship 
Starts: 
01 April 2016 
Ends: 
31 March 2021 
Value (£): 
1,005,506

EPSRC Research Topic Classifications: 
Fundamentals of Computing 


EPSRC Industrial Sector Classifications: 
No relevance to Underpinning Sectors 


Related Grants: 

Panel History: 

Summary on Grant Application Form 
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 such
models 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 considering
the 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 yet
no 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 a
system variable whose behaviour is determined by differential equation can ever enter a critical state. The main challenge in the project is that the longterm evolution of systems can be very
complex to analyse even though their shortterm behaviour is simple. The project considers a range of verification problems for different types systems, including discretetime and
continuoustime 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.

Key Findings 
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk

Potential use in nonacademic contexts 
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk

Impacts 
Description 
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk 
Summary 

Date Materialised 


Sectors submitted by the Researcher 
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk

Project URL: 

Further Information: 

Organisation Website: 
http://www.ox.ac.uk 