MRG home page Research Publications Software People

University of Edinburgh

Mechanising First-Order Temporal Logics

Project Description

This project aims at applying sophisticated reasoning techniques from Artificial Intelligence (namely Proof Planning) to the development of a practical automated reasoning system for First-Order Linear-time Temporal Logic (FOLTL).

Motivation

FOLTL offers a clear, intuitive means of encoding and representing the behaviour of complex, reactive, concurrent and parametrised infinite-state systems; in principle, it is a great choice for verification of this kind of systems.

But FOLTL is extremely hard (non recursively enumerable) and therefore any general-purpose standard theorem proving technique is probably bound to fail, at least on examples of practical interest.

Yet as these application areas are increasingly important in both mainstream computer science and Artificial Intelligence, the development of appropriate reasoning systems for such logics will ultimately contribute to many strands within these disciplines.

We claim that Proof Planning can help. Through search at an abstract level, rather than in the proof search space, Proof Planning can give an object-level FOLTL theorem prover the necessary guidance to overcome the complexity of FOLTL. This is the aim of his project.

Practical applications: Feature interactions

The most recent applications we've been working with is the Feature Interactions problem. The problem arises in large telecommunication systems such as phone networks, and represents an interesting case study for early-stage formal methods.

Informally, it is often the case that features of a telephone service, such as ring-back and automatic forwarding, clash, meaning that, upon simultaneous activation of two or more features, the system behaves in an unexpected/unwanted manner.

Formal methods such as model checking have been applied to this problem in order to detect flaws and errors in the specification, prior to the implementation phase; that is, without even having written a single line of code. This has the effect of saving time and money to the phone company.

So far, the most interesting results have been obtained by finitely approximating the network (i.e., assuming a fixed, small number of users) and model checking it; we aim at employing, at least at the higher level of abstraction, a deductive approach and no finite approximation.

People

The following people are working on the project:

Publications

All papers are available in electronic form from Claudio's publications page.

C. Castellini and A. Smaill
Proof Planning for First-Order Temporal Logic (2005)
proceedings of CADE 2005, to appear

C. Castellini
Automated Reasoning for Quantified Modal and Temporal Logics (2005)
Ph.D. thesis, School of Informatics, University of Edinburgh.
Awarded Best Italian Ph.D. Thesis 2005 by AIIA (Artificial Intelligence Italian Association)
a 2-pages summary of the thesis is to appear in the AI Communications
a longer summary (8 pages) is to appear in Intelligenza Artificiale

C. Castellini and A. Smaill
A Systematic Presentation of Quantified Modal Logics (2002)
Logic Journal of the IGPL 10(6), November 2002

C. Castellini and A. Smaill
Proof Planning for Feature Interactions: a Preliminary Report (2002)
proceedings of LPAR 2002, LNCS 2514

C. Castellini and A. Smaill
Tactic-based Theorem Proving in First-Order Modal and Temporal Logics (2001)
proceedings of Issues in the Design and Experimental Evaluation of Systems for Modal and Temporal Logics, IJCAR 2001 Workshop 10

C. Castellini and A. Smaill
A Modular, Tactic-based Approach to First-Order Temporal Theorem Proving (2000)
presented at ICTL - International Conference on Temporal Logic, Leipzig, Germany, November 2000

Links

Funding

The project was funded by EPSRC. The grant has expired in July, 2002.


Webpage maintained by Claudio Castellini