EPSRC logo

Details of Grant 

EPSRC Reference: EP/N008197/1
Title: Verification of Linear Dynamical Systems
Principal Investigator: Worrell, Professor JB
Other Investigators:
Researcher Co-Investigators:
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:
Panel DatePanel NameOutcome
09 Sep 2015 EPSRC ICT Fellowships Interview Panel - Sept 2015 Announced
15 Jul 2015 EPSRC ICT Prioritisation Panel - Jul 2015 Announced
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 long-term evolution of systems can be very

complex 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.

Key Findings
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Potential use in non-academic contexts
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Description This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
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