PhD Possibilities?

If you are seriously interested in PhD study, from the sample list below or related to my projects or publications, then first read the application procedure and guidance.

Also, please explore potential funding possibilities yourself - although the Department offers some PhD studentships these are very competitive and often restricted to EU or even UK applicants.

Finally, a PhD requires abilities such as mathematical, programming, and communication skills, analytical thinking, creativity, and self-motivation - be sure you have all these before applying.

Sample PhD Topics

Below I have listed a selection of potential PhD topics, to give you examples of the type of project I am happy to supervise. Please note that not only do they represent just a sample of possible projects but the list changes often and some of the topics might not now be available.

Deductive Verification of Security Protocols

The analysis of security protocols is difficult, even if we ignore the details of cryptography, with problems such as the "man in the middle" attack being commonplace. Formal analysis is needed in order to, if possible, uncover all potential security problems and build trust in that protocol. A lot of work has been done in this area, dating back from to Needham-Schroeder protocol and its analysis using formal techniques. We have tackled this problem by using temporal logics of knowledge to specify some protocol problems and applying resolution techniques to automatically verify these. However, this is only a start. We believe that the analysis of protocols, in particular the information flow between participants, can be elegantly captured using such logics, though possibly extended with other modalities, real-time aspects, probabilities, etc. This PhD project will assess the required improvements in the approach, develop and extend this, and apply to relevant protocols. (To be jointly supervised with Clare Dixon.)

Relevant Publication: C. Dixon, M-C. Fernández Gago, M. Fisher, and W. van der Hoek. Temporal Logics of Knowledge and their Applications in Security. Electronic Notes in Theoretical Computer Science 186:27-42. Elsevier, 2007.

Efficient Agent Verification

As agent-based solutions are used in increasingly complex and critical areas, there is a need to analyze, comprehensively, the behaviour of these systems. Not surprisingly, therefore, formal verification techniques tailored specifically for agent-based systems are also an area that is attracting a great deal of attention. Our work is at the forefront of this new area, where we have extended and adapted model checking techniques in order to be applicable to the formal verification of agent-based systems. However, these verification techniques are slow. This PhD project aims to improve efficiency (and therefore applicability) in a number of ways, including extending our initial work on property-based slicing for agent programs. (To be jointly supervised with Louise Dennis.)

Relevant Publication: R. H. Bordini, M. Fisher, M. Wooldridge, and W. Visser. Property-based Slicing for Agent Verification. Journal of Logic and Computation 19(6):1385-1425, 2009.

Extending First-Order Temporal Deduction

First-order temporal logic (FOTL) is a powerful descriptive language. Unsurprisingly, this makes it complex to reason with, the decision problem being undecidable in general. However, the monodic fragment of FOTL does have better properties. In earlier work we have developed an automated clausal resolution system for monodic FOTL and have subsequently improved the efficiency still further. In applying this logic it has become clear that yet further extension is required, particularly with real-time, probabilistic, or hybrid aspects. This is what the PhD will tackle. (To be jointly supervised with Boris Konev.)

Relevant Publication: A. Degtyarev, M. Fisher, and B. Konev. Monodic Temporal Resolution. ACM Transactions on Computational Logic 7(1):108-150. ACM, January 2006.

Distributed Theorem-Proving

For decades computer scientists could rely on exponential increases in processor speed, closely linked to the exponential increase in the number of transistors and their exponential miniaturisation predicted by Moore's law, to ensure that more and more complex and challenging problems eventually become solvable in reasonable time on commonly available hardware. However, in recent years, increases in the number of transistors have no longer translated into exponentially greater speed, but instead into a greater number of computing cores capable to execute a larger number of parallel threads. At the same time the increasingly widespread use of the Internet has led to a number of new computing paradigms like grid computing, cloud computing and P2P computing. These changes have reinvigorated interest in various forms and applications of distributed computing, including distributed theorem proving, which had attracted a lot of attention in the late 1990s. The aim of this project is to explore novel agent-based approaches to distributed theorem-proving. Initially the project will start with a survey of the existing body of work, including our own, and will then evolve to tackle different models of distributed theorem proving and will try to target a variety of logics including propositional, first-order and non-classical logics. (To be jointly supervised with Ullrich Hustadt.)

Relevant Publication: M. Fisher. Multi-Agent Programming Based on Distributed Deduction. In Distributed Constraint Problem Solving and Reasoning in Multi-Agent Systems, volume 112 of Frontiers in Artificial Intelligence and Applications. IOS Press, November 2004.

Contexts, Organisations and Mobility

The modelling of context is vitally important to many areas of computing, including pervasive systems, mobility, organisational modelling, multi-agent systems, etc. Thus there have been a number of approaches to capturing this. Some are specific to one aspect, such as mobility, e.g. bigraphs or organisational roles, while others model contexts as complex ontologies. Our approach is slightly different. We provide an active agent with access, at any particular moment in time, to the contexts it resides in and the contents that reside within it. We wish to analyse our model and contrast it with others. This has been initially explored in a previous PhD but the aim of this PhD project is to carry out such comparisons in greater depth, assess how our approach can be productively extended/restricted, and assess how our work can impact upon the other approaches.

Relevant Publication: A. Hepple, L. A. Dennis, and M. Fisher. A Common Basis for Agent Organisations in BDI Languages. Lecture Notes in Artificial Intelligence 5118, pages 171-88. Springer, 2008.

Computation and Control

Within Computer Science we study a range of problems, typically comprising discrete abstractions of real-world phenomena. However, our programs must interact with more complex systems, not only the real environment but possibly with other electronic or mechanical devices. We have methods of formalising the activities within our systems/programs, for example formal logics, while the developers of the real/complex systems have their own methods, ranging from control systems to Markov processes. Within this project we aim to investigate better, and more intuitive, ways to interact with complex systems. This will comprise both a theoretical analysis and further work on the impact of this analysis on ways of programming and verifying real systems. This will address a number of aspects, including current ways of (formally) interacting with complex systems, ways of abstracting from complex dynamics and applying verification, programming or synthesis techniques, and current work on agent abstractions for interacting with control systems. (To be jointly supervised with Alexei Lisitsa.)

Relevant Publication: L. A. Dennis, M. Fisher, A. Lisitsa, N. Lincoln, and S. M. Veres. Satellite Control Using Rational Agent Programming. IEEE Intelligent Systems 25(3):92-97, May/June, 2010.

Deductive Verification of Swarm Robotic Behaviours

In collaboration with the Bristol Robotics Lab, we have been looking at the formal verification of swarm robotic behaviours. The formal models are based on the simple state-machine views provided by the robotics experts, which we then represent using temporal logic statements. Proofs about the system are then generated automatically via clausal temporal resolution. However, there are many aspects that we have abstracted from, including uncertainty, real-time constraints, and the arbitrary size of robotic swarms. These will all be considered within this PhD project. (To be jointly supervised with Clare Dixon.)

Relevant Publication: C. Dixon, M. Fisher, A. Winfield, and C. Zeng. Towards Temporal Verification of Swarm Robotic Systems. To appear in Robotics and Autonomous Systems, 2012.

Michael Fisher [Department of Computer Science, University of Liverpool]