MSc Projects offered by Ullrich Hustadt (2010-11)

If you have any further questions concerning one of these projects, please contact me.

UH-G1: A Testbench for Theorem Provers

Overview:
Our research group is internationally renowned for its work on temporal theorem proving calculi and the development of implementations of such calculi, e.g. the TRP system, TRP++ system, and the XA system (developed by one of our past MSc students).

Like any other software system, these systems have to be tested, and, in addition, they have to be compared to similar systems to evaluate their performance. Such performance evaluations are typically performed by running the various systems on hundreds or thousands of benchmark systems. Obviously, this is a task that support by sort of testbench, which allows us to run a whole series of benchmarks at the push of a button.

Aims:
The aim of this project is to (i) implement a generator for benchmark problems, (ii) implement a testbench program which can execute theorem proving systems on collections of benchmarks, and (iii) conduct an evaluation of given theorem proving systems using the software developed in tasks (i) and (ii).

There are several levels of sophistication that the testbench could reach. A minimalist system would be a Java program which executes on a local PC an external theorem proving system on a series of benchmark problems. A more advanced testbench would distribute the execution over a cluster of PCs. The most sophisticated testbench would in addition provide up-to-date information on the distributed test runs and perform an analysis of the results of these runs.

Requirements:
A basic understanding of temporal logic, UNIX process handling, and good knowledge of Java is required. Knowledge of Java Remote Method Invocation would be an advantage or would need to be acquired. Likewise, knowledge of Java GUI development and regular expressions could prove useful.
Supervison:
First supervisor: Ullrich Hustadt
Second supervisor: Clare Dixon, Boris Konev, or Alexei Lisitsa
Assessor: TBA

UH-G2: A Theorem Prover for PDL

Overview:
In the module COMP525, Reasoning About Action and Change, the logic PDL was studied. This project involves the development of a theorem prover for PDL. In particular, the prover should take a PDL formula as input, construct a tableaux for that formula and perform a so-called eventuality check after each branch of the tableaux has been completed.
Aims:
The aim of this project is to develop a theorem prover for PDL based on the procedure outlined above in a language of the student's choice.
Requirements:
An understanding of PDL and good knowledge of a programming language is required.
Supervison:
First supervisor: Ullrich Hustadt
Second supervisor: Clare Dixon or Boris Konev
Assessor: TBA

UH-R1: Search Optimisation for Modal Tableaux Provers

Overview:
Modal logics are extensions of propositional logic by two additional operators: `Box' and `Diamond'. Their semantics is given by Kripke models, which are basically graphs where nodes are annotated by propositions. Modal Tableaux Provers can be seen as systems which, given a modal formula, search for a Kripke model satisfying the given formula, if such a model exists. This search process is not unsimilar to finding a way through a labyrinth with a start point at the root of the tree and one or more end points / exits being at leaves of the tree.

In its simplest form the search process can be done by chronological backtracking. Here one moves from the root down various branches until one reaches one of the leaves. If this leave turns out to be an end point / exit, then the process is completed. However, if not, then one has to `backtrack' to an earlier branch point and head down a different branch. In chronological backtracking the branch point is the first unexplored branch point when coming back from the last leave one has explored.

However, there are cleverer methods like conflict-directed backjumping, dependency directed backtracking or dynamic backtracking which try to avoid exploring parts of the tree which are known not to include an end point / exit.

Methods for this have been discribed in some detail in Zhen Li, "Efficient and Generic Reasoning for Modal Logics", PhD thesis, School of Computer Science, University of Manchester, 2008.

Aims:
The task of this project is to provide a Java implementation of the methods described in this thesis and to conduct experiments that compare the effectiveness of different forms of backtracking.
Requirements:
An understanding of modal logic and a good basic knowledge Java is required. Knowledge of Java classes and methods relevant for the development of data structures will need to be acquired and are crucial for the success of this project.
Supervison:
First supervisor: Ullrich Hustadt
Second supervisor: Clare Dixon or Boris Konev
Assessor: TBA

UH-R2: A (Temporal Logic) Model Generator

Overview:
A central problem in any logic is to determine whether a given formula is satisfiable, i.e. whether there is a model in which the formula is true. Typically, for each logic there is a range of calculi which can be used to this end. Examples are tableaux calculi and resolution calculi.

While tableaux calculi can be seen to attempt to directly construct a model for a given formula, resolution calculi typically attempt to characterise the set of all models for a given formula. Although this is an advantage in a range of applications, in the context of verification problems, it is often desirable to have an explicit representation of the set of models or a single model.

Aims:
The task of this project is to implement a program which, given a formula or set of clauses produces a graphical representation of the set of all models or a single model.
  • If the logic under consideration would be linear time temporal logic, then the approach described by Fisher, Dixon, Peim (2001) could be used to create first a behaviour graph and then a reduced behaviour graph for a set of SNF clauses.
  • If the logic under consideration would be propositional logic or a fragment of first-order logic, then the approach would be implement a simple resolution prover and to use the standard model construction for the saturated set of clauses (see, for example, the slides by Harald Ganzinger for the module Logic for Computer Science, 2002).

The choice of the logic will be up to the student.

Requirements:
Depending on the logic, a good understanding of the logic is required as well as a good basic knowledge Java. Knowledge of Java classes and methods relevant for the development of graphical user interfaces will need to be acquired and are crucial for the success of this project.
Supervison:
First supervisor: Ullrich Hustadt
Second supervisor: Clare Dixon or Boris Konev
Assessor: TBA