Projects [Michael Fisher]

Potential Projects

Michael Fisher

Department of Computer Science, University of Liverpool

EMAIL: M.Fisher@csc.liv.ac.uk

Tel: (+44) 151 794 6701 Fax: (+44) 151 794 3715

The projects outlined below are available for supervision by Michael Fisher. In addition, students interested in projects in the general areas of Formal Methods, Logic, Artificial Intelligence, Agents and Concurrency are welcome to contact Michael Fisher.

Michael Fisher is available to discuss project proposals at either of the following times

15:00-17:00	Tuesday 13th May
09:00-11:00	Tuesday 20th May

The projects described below can be summarised as follows:

Research
: MDF1R: Promela to Temporal Logic Translation
: MDF2R: Legolog and METATEM
: MDF3R: Efficient Transformation to SNF
: MDF4R: Partitioning Proofs

Problem-Solving
: MDF1P: Micro Java Model Checker
: MDF2P: Multi-Agent Implementation of METATEM
: MDF3P: User Interface for a Temporal Resolution System
: MDF4P: Verification of Concurrent METATEM
: MDF5P: Implementing Multi-Agent Theorem-Proving

Development
: MDF1D: Java Classes for Temporal Formula Representation
: MDF2D: Animating Omega-Automata
: MDF3D: Enquiry System for Liverpool Verification Laboratory

Research

MDF1R: Promela to Temporal Logic Translation

Model Checking is a technique by which a finite state structure describing the behaviours of a program can be checked against a temporal logic specification. In many model checking approaches, appropriate finite state programming languages are provided with the model checking tool. A well known example is the PROMELA language used to model finite state systems. This is the basic input to the Spin system [1], one of the most successful model checkers.

However, there are alternatives to model checking that can be used to verify properties of programs. In particular, a temporal semantics may be given to languages such as PROMELA and temporal theorem-proving can then be applied [2]. The aim of this project is to (a) provide a tool for translating Promela into temporal logic, and then (b) to provide a mechanism whereby such temporal formulae can be adapted to be appropriate input for temporal provers (e.g. [3]).

G. Holzmann. The Model Checker Spin. IEEE Trans. on Software Engineering 23(5):279-295, 1997.
Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer-Verlag, 1992.
B. Konev. and U. Hustadt. TRP++: A Temporal Resolution prover. In Proc. International Workshop on Implementation of Logics, 2002.

MDF2R: Legolog and METATEM

Legolog [1] is a Prolog-based system developed to allow experimentation with the Lego Mindstorms Robotics Invention System [2]. This is intended to allow interaction between programming languages implemented in Prolog and Lego robots.

METATEM is a programming language based on the direct execution of temporal logic specifications [3], which is currently implemented in Prolog.

The aim of this project is attempt to interface METATEM with Legolog and thus use METATEM to control Lego robots.

Legolog http://www.cs.toronto.edu/cogrobo/Legolog
Lego Mindstorms. http://mindstorms.lego.com
M. Fisher. Implementing BDI-like Systems by Direct Execution. In M. Pollack, editor, Proceedings of International Joint Conference on Artificial Intelligence (IJCAI'97). Morgan-Kaufmann, 1997.

MDF3R: Efficient Transformation to SNF

Just as in classical logic where the transformation process from arbitrary formulae to clausal form is vital, the transformation from arbitrary temporal formulae to separated normal form (SNF) [1] is important in temporal reasoning. We have defined various transformations that may be used to completely transform a formula into SNF, but there are a number of ways in which such transformations can be combined [2].

The aim of this project is to design and implement a system for carrying out the above transformations, to experiment with different ways of carrying out the transformation and to evaluate each of these approaches.

M. Fisher. A Normal Form for Temporal Logic and its Application in Theorem-Proving and Execution. Journal of Logic and Computation 7(4), July 1997.
M. Fisher, C. Dixon, and M. Peim. Clausal Temporal Resolution. ACM Transactions on Computational Logic, 2(1), January 2001.

MDF4R: Partitioning Proofs

Theorem proving for classical propositional logic is quite simple to understand. However, it is difficult to implement efficiently. It is often the case that the number of formulae dealt with during a proof is too large to be handled easily. Thus, a great many strategies, especially in the predominant clausal resolution approach, have involved trying to reduce the amount of clauses (formulae) considered.

In a previous M.Sc. project, concerning multi-agent theorem-proving [1], a technique was developed for partitioning sets of clauses amongst distributed agents. However, this technique was never fully tested. Rather than developing a full multi-agent theorem-prover, the aim of this project is to implement the algorithm for partitioning sets of clauses, and then use these partitions as input to a standard resolution prover. In this way, the effectiveness of the partitioning strategy can be assessed.

Thus, the project will provide a tool which translates a proof problem given in a standard format (e.g. supported within the TPTP library of problems [2]), partitions the clauses within this problem, and calls an appropriate resolution prover on each of these partitions. It may be necessary to repeat this process a number of times.

The intention is to use a standard resolution prover, e.g. Otter [3], SPASS [4] or Vampire [5], and to produce all the required statistics in an appropriate format.

H. Kampmann. Implementing Multi-Agent Theorem-Proving. M.Sc. Thesis, Department of Computing and Mathematics, Manchester Metropolitan University, 1998.
The TPTP Problem Library for Automated Theorem Proving. http://www.cs.miami.edu/ tptp
Otter: An Automated Deduction System. http://www-unix.mcs.anl.gov/AR/otter
SPASS: An Automated Theorem Prover for First-Order Logic with Equality. http://spass.mpi-sb.mpg.de
Vampire - A Theorem Prover for First-Order Classical Logic. http://www.cs.man.ac.uk/ riazanoa/Vampire

Problem-Solving

MDF1P: Micro Java Model Checker

Model Checking [1] is a technique by which a finite state structure describing the behaviours of a system (typically a program) can be checked against a temporal logic formula. The temporal formula is automatically checked against this structure in order to determine whether the structure does actually represent a model for the formula, in which case we can say that the system itself satisfies the property captured by the formula.

In [2], we specified a simple model checker and implemented it in C. As part of an M.Sc. project in 2002, this model checker was re-implemented in Java [3]. Now we wish to (a) modify the implementation so that it can be implemented using J2ME, a variety of Java designed for small devices [4], and (b) test the implementation, and evaluate it on benchmark scenarios for model checkers.

E. Clarke, O. Grumberg, and D. A. Peled. Model Checking. MIT Press, 2000.
M. Fisher. A Model Checker for Linear Time Temporal Logic. Formal Aspects of Computing, 4(3):299-319, June 1992.
A. Hepple. Java Model Checker. MSc Dissertation. Department of Computer Science, University of Liverpool. 2002.
Java 2 Platform, Micro Edition. http://java.sun.com/j2me

MDF2P: Multi-Agent Implementation of METATEM

METATEM is a programming language based on the direct execution of temporal logic specifications [1]. This approach provides a tight link between specification and implementation within systems development.

A temporal specification is executed, using the Imperative Future paradigm [2], simply by applying an iterative forward-chaining process to the temporal formula characterising the specification. Currently, the basic METATEM system is implemented in Prolog.

The aim of this project is to extend this implementation to a multi-agent environment. The two aspects of this project are: (a) implement multiple METATEM interpreters communicating with each other; and (b) develop a library of multi-agent examples for this system. There are a number of ways to achieve (a): use the multi-threading features of Prolog (e.g. [3]); use a ``Prolog in Java'' translator [4] and capture the multi-agent aspects in Java, or use a ``Prolog to Java'' link [3] and again use Java to link separate Prolog engines.

M. Fisher. Implementing BDI-like Systems by Direct Execution. In M. Pollack, editor, Proceedings of International Joint Conference on Artificial Intelligence (IJCAI'97). Morgan-Kaufmann, 1997.
H. Barringer, M. Fisher, D. Gabbay, R. Owens, and M. Reynolds, editors. The Imperative Future: Principles of Executable Temporal Logic. Research Studies Press, 1996.
SWI Prolog. http://www.swi-prolog.org
Prolog Café. http://kaminari.scitec.kobe-u.ac.jp/PrologCafe

MDF3P: User Interface for a Temporal Resolution System

Given a temporal logic formula, there are a number of ways in which the truth or falsity of the formula can be established. A particular approach developed within the Department is that of using clausal temporal resolution [1]. An efficient system based on this approach has been implemented; this is called TRP++ and it is implemented in C++ [2].

While the TRP++ is efficient, it is not yet easy to use. Thus, the aim of this project is to develop an appropriate and usable user interface for the system. This should incorporate a mechanism for inputting and parsing temporal formulae, an extensible library of predefined temporal problems, and an intuitive way of presenting the output to the user. All this should be provided within an appropriate Java interface.

M. Fisher, C. Dixon, and M. Peim. Clausal Temporal Resolution. ACM Transactions on Computational Logic, 2(1), January 2001.
B. Konev. and U. Hustadt. TRP++: A Temporal Resolution prover. In Proc. International Workshop on Implementation of Logics, 2002.

MDF4P: Verification of Concurrent METATEM

While METATEM is a programming language based on the direct execution of temporal logic specifications [1], Concurrent METATEM is a concurrent framework in which many METATEM agents can execute and communicate [2]. This language provides a simple mechanism for programming multi-agent computation via the execution of multiple temporal specifications. Concurrent METATEM is implemented in C++.

The aim of this project is to provide a tool which can translate a Concurrent METATEM program (essentially a set of executable temporal specifications) into one single temporal logic formula representing the behaviour of the whole system. This formula should be in a form suitable for input into a temporal theorem-prover (specifically, TRP++ [3]). In this way, the behaviour of the Concurrent METATEM program can be verified as well as executed.

M. Fisher. Implementing BDI-like Systems by Direct Execution. In M. Pollack, editor, Proceedings of International Joint Conference on Artificial Intelligence (IJCAI'97). Morgan-Kaufmann, 1997.
M. Fisher. A Survey of Concurrent METATEM -- The Language and its Applications. Lecture Notes in Computer Science, volume 827, Springer-Verlag, 1994.
B. Konev. and U. Hustadt. TRP++: A Temporal Resolution prover. In Proc. International Workshop on Implementation of Logics, 2002.

MDF5P: Implementing Multi-Agent Theorem-Proving

Theorem proving for classical propositional logic is quite simple to understand. However, it is difficult to implement efficiently. This is due to the large range of possibilities that must be explored. Not surprisingly, concurrency has been suggested as a route to more efficient theorem-proving. Typically, the concurrent theorem-proving techniques that have been developed have relied on standard, fairly inflexible models of concurrency. The concurrent processes are globally controlled and are thus not autonomous.

We have proposed a new method for concurrent theorem-proving based on the use of a multi-agent approach [1]. An agent can be seen as an autonomous computational entity with a (possibly limited) form of `intelligence'. In a previous M.Sc. project, Heiko Kampmann developed a C++/Unix implementation of this approach, together with algorithms for distributing formulae to agents [2].

The aim of this project is to re-implement the system in (multi-threaded, but not distributed) Java, and to test it on a wider range of examples.

M. Fisher. An Open Approach to Concurrent Theorem-Proving. In J. Geller, H. Kitano, and C. Suttner, editors, Parallel Processing for Artificial Intelligence, volume 3. Elsevier/North-Holland, 1997.
H. Kampmann. Implementing Multi-Agent Theorem-Proving. M.Sc. Thesis, Department of Computing and Mathematics, Manchester Metropolitan University, 1998.

Development

MDF1D: Java Classes for Temporal Formula Representation

A key logical formalism used within Formal Methods is temporal logic [1]. Temporal logic is an extension of classical logic, whereby time becomes an extra parameter when considering the truth of logical statements. We apply temporal logic in a number of ways (e.g. verification [2] and execution [3]) and have constructed several tools to support this.

The aim of this project is to re-design and re-implement the core classes which represent temporal formulae, together with methods that apply simple transformations to these formulae. The existing temporal formulae package is implemented in C++ and this project will re-implement the package in Java, taking advantage of as many of Java's features as may be appropriate. The Java package will then be tested and evaluated.

E. Emerson. Temporal and Modal Logic. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, pages 996-1072. Elsevier, 1990.
M. Fisher, C. Dixon, and M. Peim. Clausal Temporal Resolution. ACM Transactions on Computational Logic, 2(1), January 2001.
H. Barringer, M. Fisher, D. Gabbay, G. Gough, and R. Owens. METATEM: An Introduction. Formal Aspects of Computing, 7:533-549, 1995.

MDF2D: Animating Omega-Automata

Automata over infinite objects, termed omega-automata, were originally introduced as a tool for investigating the decidability of restricted classical first-order and second-order logics [1,2], but have also been extensively used in recent developments within wider areas of Computer Science. However, such automata are often hard to visualise.

The aim of this project is to provide a graphical representation of such automata and to provide a mechanism for animating the automaton by providing input that it might recognise.

J. R. B¨uchi. On a decision method in restricted second-order arithmetics. In Proc.of International Congress of Logic, Methodology and Philosophy of Science, Stanford University Press, pages 1-12, 1962.
W. Thomas. Languages, automata, and logic. In Handbook of Formal Language Theory, volume III, Elsevier Science Publishers, Amsterdam, 1997.

MDF3D: Enquiry System for Liverpool Verification Laboratory

The Liverpool Verification Laboratory is a new activity within the Department of Computer Science. The idea of this initiative is to provide a centre where industrial verification problems can be tackled using sophisticated techniques developed within the Department.

The Laboratory already has a very minimal WWW site [1], but a more sophisticated mechanism for handling (and logging) enquiries sent to the Laboratory is needed. The aim of this project is to develop a WWW interface through which enquiries can be entered; such enquiries may also involve various attachments. The enquiries need to be processed, recording them in a database, automatically replying to the enquirer, and sending summaries on to the directors of the Laboratory.

Liverpool Verification Laboratory. http://www.csc.liv.ac.uk/liverlab

About this document ...

Potential Projects

This document was generated using the LaTeX2HTML translator Version 2002 (1.62)

The command line arguments were:
latex2html -no_subdir -split 3 -no_navigation -address M.Fisher@csc.liv.ac.uk projects

The translation was initiated by Michael Fisher on 2003-05-06

M.Fisher@csc.liv.ac.uk