Research
Verification of robotic systems
The formalisation and analysis of robotic systems using formal verification. Formal verification involves a mathematical analysis of all behaviours using logics, and tools such as theorem provers or model checkers. Theorem provers involve mathematical proof in an appropriate logic. Model checkers are an automated, exhaustive algorithmic technique to check properties of a system over its state space. We have applied such techniques to robot swarms (groups of simple robots), robotic assistants and robots operating in extreme environments to make sure they are reliable, safe, trustworthy and achieve their purpose.
Automated reasoning for temporal and modal logics
The development, application and experimentation with calculi and related theorem provers for a variety of modal, temporal and agent logics. A variety of logics have been developed to capture and model particular aspects of the world. Here we develop calculi to mechanise reasoning via theorem proving. We apply the developed provers to particular domains and experiment with them.
Verification and Validation for Security
I am interested in applying logical techniques to aspects of security. Recent work has applied formal verification to autonomous systems based on threat analysis techniques (with the University of Warwick). Another project considers modelling and validation of security protocols using Abstract State Machines. Earlier work relates to signature based Intrusion Detection where attacks are specified using temporal logics. These are translated into data stream queries and stream data processing systems are used to identify attacks.
Research grants
Robotics and Artificial Intelligence for Nuclear - RAIN
ENGINEERING & PHYSICAL SCIENCES RESEARCH COUNCIL
October 2017 - September 2021
Science of Sensor System Software.
ENGINEERING & PHYSICAL SCIENCES RESEARCH COUNCIL
January 2016 - December 2021
Future AI and Robotics for Hub Space (FAIR-SPACE)
ENGINEERING & PHYSICAL SCIENCES RESEARCH COUNCIL
November 2017 - March 2021
Trustworthy Robotic Assistants
ENGINEERING & PHYSICAL SCIENCES RESEARCH COUNCIL
March 2013 - August 2016
Research collaborations
Michael Fisher
Joint papers and projects in the area of verification and logics
Ullrich Hustadt
Joint papers and projects in the area of logics and automated reasoning.
Alexei Lisitsa
Joint papers in the area of security
Claudia Nalon
University of Brasilia
Joint papers in the area of logics and automated reasoning