Theorem Proving for Temporal Logics
Primary supervisor
Additional supervisors
- Marie Farrell
Additional information
- [1] Dimitra Giannakopoulou, Thomas Pressburger, Anastasia Mavridou, Julian Rhein, Johann Schumann, Nija Shi, Formal Requirements Elicitation with FRET, REFSQ Workshops 2020
- [2] Dixon, C., Konev, B., Fisher, M. and Nietiadi, S., Deductive temporal reasoning with constraints, Journal of Applied Logic. 11, 1, p. 30-51, 2013
- [3] Fisher, M., Dixon, C. & Peim, M., 2001, Clausal Temporal Resolution, ACM Transactions on Computational Logic.
- [4] Hustadt, U and Konev, B, TRP++2.0: A Temporal Resolution Prover. CADE 2003: 274-278
- [5] Hustadt, U., Ozaki, A. & Dixon, C., Theorem Proving for Pointwise Metric Temporal Logic Over the Naturals via Translations Journal of Automated Reasoning. 64, 8, p. 1553-1610, 2020
- [6] Li, J., Vardi, M.Y., Rozier, K.Y.: Satisfiability checking for mission-time ltl (mltl). Information and Computation 289, 104923 (2022)
- [7] Nalon, C., Hustadt, U. & Dixon, C., A Resolution-Based Theorem Prover for Kn, Kn: Architecture, Refinements, Strategies and Experiments Journal of Automated Reasoning, 2020
- [8] Nalon, C., Dixon, C. & Hustadt, U., Modal Resolution: Proofs, Layers and Refinements ACM Transactions on Computational Logic. 20, 4, 23, 2019.
Contact admissions office
Other projects with the same supervisor
- Formal Verification of Robot Teams or Human Robot Interaction
- Formal Verification for Robot Swams and Wireless Sensor Networks
Funding
- 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
- Candidates must hold a minimum of an upper Second Class UK Honours degree or international equivalent in a relevant science or engineering discipline.
- Candidates must meet the School's minimum English Language requirement.
- Candidates will be expected to comply with the University's policies and practices of equality, diversity and inclusion.
Essential
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.
Desirable
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.
General
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?