EPSRC logo

Details of Grant 

EPSRC Reference: EP/V025848/1
Title: COSTRA -- The Cost of Winning Strategies
Principal Investigator: Totzke, Dr P
Other Investigators:
Researcher Co-Investigators:
Project Partners:
Keysight Technologies Inc
Department: Computer Science
Organisation: University of Liverpool
Scheme: New Investigator Award
Starts: 01 July 2021 Ends: 28 September 2024 Value (£): 349,044
EPSRC Research Topic Classifications:
Fundamentals of Computing
EPSRC Industrial Sector Classifications:
Information Technologies
Related Grants:
Panel History:
Panel DatePanel NameOutcome
02 Dec 2020 EPSRC ICT Prioritisation Panel December 2020 Announced
Summary on Grant Application Form
We investigate mathematical models of computation, which is a necessary precondition to understand and explain the behaviour of AI systems and other computer programs.

Cyber-physical systems increasingly affect most aspects of our lives: they are used in pacemakers, manage factory supply chains, trade in stocks and autonomously pilot modern planes and cars. Software deficiencies can have serious economic and life-threatening consequences. While traditional methods of testing and simulations can be effective for finding errors, they are hopelessly inadequate for showing their absence. A more promising approach is to use mathematical arguments to prove that a system behaves as intended, in all possible situations. Verification is the area of research based on this idea. It is truly interdisciplinary and has fascinating connections to Artificial Intelligence, Discrete Mathematics and Software Engineering.

To prove the correctness of some system one starts with a formal model of the system itself as well as a specification that defines what correctness means. In model-checking, for instance, we model systems as a finite-state machine and the specifications as temporal logic formulae. Correctness then ammounts to the fact that the finite-state machine satisfies the formula, which can often be verified automatically. Naturally, there are many different ways to formalize systems and specifications, and some formalisms are more expressive than others.

Current methods are very good at analysing models with only finitely many internal configurations, such as microchips or hardware drivers. However, if we move to more expressive models we quickly go beyond the reach of known techniques or even cross theoretical limits. At this point the research frontier is on so-called infinite-state models, which enable us to argue directly about unbounded quantities such as realtime constraints, recursion depth or simultaneous user requests.

For example, imagine a network server that can receive any number of requests concurrently and which should eventually respond to all of them. The total number of requests is not determined in advance and so it is necessary to incorporate it into the model, which consequently has infinitely many possible internal configurations. However, we do have good finite representations, such as Counter Machines or Pushdown Automata, that can be used in such situations. The result is a trade-off between the expressibility of these formalisms and the feasibility of their verification.

A key mathematical tool for correctness checks and decision making in the presence of environmental uncertainty are games between antagonistic players, who try to cause and prevent errors, respectively. Closely related formalisms are used in Economics, Biology, Chemistry and other sciences, in the form of Markov Chains and Markov Decision Processes.

Correctness here corresponds to the existence of winning strategies, which tell their player how to move in order to secure a win. Winning strategies are important not only because they act as correctness certificates but also because they can often be directly translated into executable code.

Our research seeks to understand more general, infinitary strategies, which are often necessary for realistic specifications. We will investigate the mathematical structure, internal complexity, and thus the cost of winning strategies. Advancing our understanding of strategies promises to yield better finite representations, which in turn makes it easier to verify that winning strategies exist (checking correctness) as well as automatically generating and executing them.

Our research leads to a deeper understanding of the nature of computation and decision making and provides new and improved methods for automated program verification.
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.liv.ac.uk