Mobile menu icon
Skip to navigation | Skip to main content | Skip to footer
Mobile menu icon Search iconSearch
Search type

Department of Computer Science

Theorem Proving for Temporal Logics

Primary supervisor

Additional supervisors

  • Marie Farrell

Additional information

Contact admissions office

Other projects with the same supervisor


  • Competition Funded Project (Students Worldwide)

This research project is one of a number of projects at this institution. It is in competition for funding with one or more of these projects. Usually the project which receives the best applicant will be awarded the funding. Applications for this project are welcome from suitably qualified candidates worldwide. Funding may only be available to a limited set of nationalities and you should read the full department and project details for further information.

Project description

Temporal logics are useful for specifying and verifying systems that change over time.
In [3] we describe a calculus for theorem proving in propositional linear time temporal (LTL) logics based on resolution. Here a translation to a normal form is utilise that reduces the number of operators that have to be considered and where formulae either occur in the initial state or everywhere. This was implemented in the prover TRP++[4].
The aim of this project is to re-visit the calculus and implementation to develop and analyse improvements and extensions and apply them to systems. Suggestions are as follows.
* In [8] the a resolution calculus for the basic modal logic K has been developed and implemented that rather than using a normal form that constructs formulae that hold in it the initial state or everywhere uses the distance from the initial state. This cuts down the number of applications of the resolution rules that need to be applied making the prover more efficient. The idea is to see to what extent this approach could be applied in temporal logics as models can be represented as an initial prefix followed by a loop.
* The slow part of the calculus is the implementation of the so-called loop finding rule. Reconsider this and develop new algorithms.
* In [2] we considered adding operators that allowed "exactly one of a number of disjuncts" often needed when specifying systems. This would add such a possibility to the calculus and implementation.
* Metric Temporal Logic (MTL) allows the temporal operators from LTL to have intervals over which the operators hold. In [5] we considered different transitions from a natural numbers model of temporal logics into LTL and experimented on these. A related logic is Mission Time temporal Logic [6]. This extension would aim to develop a calculus for the natural numbers models for one of these logics, implement and analyse it.
* FRET is a specification tool [1] that can be used to input temporal formulae via a particular languge. Here we aim to extend the tool to pass to one or more temporal provers to check the specifications are satisfiable and provide feedback to users about models.

Person specification

For information


Applicants will be required to evidence the following skills and qualifications.

  • This project requires mathematical engagement and ability substantially greater than for a typical Computer Science PhD. Give evidence for appropriate competence, as relevant to the project description.
  • You must be capable of performing at a very high level.
  • You must have a self-driven interest in uncovering and solving unknown problems and be able to work hard and creatively without constant supervision.


Applicants will be required to evidence the following skills and qualifications.

  • You will have good time management.
  • You will possess determination (which is often more important than qualifications) although you'll need a good amount of both.


Applicants will be required to address the following.

  • Comment on your transcript/predicted degree marks, outlining both strong and weak points.
  • Discuss your final year Undergraduate project work - and if appropriate your MSc project work.
  • How well does your previous study prepare you for undertaking Postgraduate Research?
  • Why do you believe you are suitable for doing Postgraduate Research?