max planck institut

informatik

informatik

**MPI-I-92-213**. March** **1992, 166 pages. | Status:** **distribution forbidden | Next --> Entry | Previous <-- Entry

Abstract in LaTeX format:

The following is a draft version of the first six chapters of a

book which is attempting to supply a comprehensive coverage of

the mathematical and computational aspects of temporal logic.

The first chapter introduces temporal logic and gives a fairly

detailed preview of the issues which will be covered in the rest

of the whole book. These include expressive power, fixed point

temporal languages and applications in computing. Chapter 2

develops the basic idea of a language built from connectives

whose semantics is appropriate to some class of underlying

"`models"' of time: for example linear or branching time.

Chapter 3 introduces Hilbert style axiomatizations of such

logics and contains some simple completeness proofs. The

incomplete chapter 4 considers the generally incomplete

predicate temporal languages and gives examples of some of the

variety of choices of language here. In Chapter 5 we debate the

merits of using classical first order logic to talk about

temporal structures from the "`outside"' instead of using

temporal languages "`inside"' the structure. We also consider

the possibility of using temporal logic itself as a

metalanguage. Finally, in Chapter 6 we present a general theory

of axiomatization of temporal logics. This examines and uses the

irreflexivity rule of Gabbay to provide very general

techniques.

Note:

Since the publication of the book (Gabbay, D. M.; Hodkinson, I.; Reynolds, M. : "Temporal logic: mathematical foundations and computational aspects",

Oxford : Clarendon 1994), this work is no longer available as report.

Acknowledgement:** **

References to related material:

An Oxford University Press Book is available: Dov M. Gabbay,Mark Reynolds,Ian Hodkinson: Temporal Logic