Temporal Logic Resources

Appeared in Volume 6/2, May 1993

mb108@cs.city.ac.uk
omo Adelakun T K
27th January 1993

Sometime ago, I asked: can anyone point me to a very good text on temporal logic? Does anyone know of a temporal logic interpreter? Something along the lines of Prolog, or an extension? This is a summary of the responses I received.

From: cmenzel@kbssun1.tamu.edu (Chris Menzel)

J. van Bentham, The Logic of Time, Reidel, 1983
A model-theoretic investigation into the varieties of temporal ontologies and their logics.

From: Shinji Kono <kono@csl.sony.co.jp

Robert Goldblatt, CSLI Lecture Notes, Logic of Time and Computation, CSLI, Vol. 7, 1987

There are many temporal logic interpreters:

1.Tokio, based on interval temporal logic, which I wrote. It is supported by both an interpreter and a compiler. It is close to Tempura, but supports non-deterministic execution.

M. Fujita and S. Kono and H. Tanaka, Tokio: LP Language based on Temporal Logic and its compilation to Prolog, Proc. of Int. Conf. on LP, London, July 1986

2. Temporal Prolog.

3. IB-Templog. Both (2) and (3) support McDermott's interval temporal logic. You can find an article about (3) in the Journal of LP.

4. Sakura's Temporal Prolog Supports linear time temporal logic.

5. Molog. A modal logic extention of Prolog. There is an article in New Generation Computing.

From: rwsh@cam.sri.com (Roger Hale)

Prior, A. N., Past, Present and Future, Clarendon Press, Oxford, 1967

Manna, Z. and Pnueli, A., The Temporal Logic of Reactive and Concurrent Systems: Specification, Springer-Verlag, 1992

Rescher & Urquhart, Temporal Logic, Springer-Verlag.

Kroger, Temporal Logic of Programs, Springer-Verlag.

Temporal Logics and Their Applications, Galton, A. (ed.), Academic Press, London, 1987

Moszkowski, B. C., Executing Temporal Logic Programs, Cambridge Univ. Press, Cambridge, England, 1986

Hale, R. W. S., Programming in Temporal Logic, Computer Laboratory, Univ. of Cambridge, England, No. 173, 1989

Abadi, M. and Manna, Z., Temporal LP, Proc. IEEE Symposium on LP, 1987

Gabbay, D. M., The Declarative Past and Imperative Future: Executable Temporal Logic for Interactive Systems, In Temporal Logic in Specification, Banieqbal, B. and Barringer, H. and Pnueli, A. (eds.), LNCS, No 398, Springer-Verlag, Berlin, 1989

From: johnson@minster.york.ac.uk

I've got a version of the Tokio interpreter, which I can mail you. For references you might try to get a copy of my thesis - it contains a huge literature survey.

A Formal Approach To The Integration Of Human Factors And Systems Engineering, C.W. Johnson, PhD Thesis, Dept. Of Computer Science, Univ. of York, York, UK, 1992

or:

Applying Temporal Logic To Support The Specification And Prototyping Of Concurrent Multi-User Interfaces, C.W. Johnson, In People And Computers VI: Usability Now, pp. 145-156, D. Diaper and N. Hammond (eds.), Cambridge Univ. Press, Cambridge, UK, 1991