| 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: |
|
|
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
|
|
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 |