MPI-I-92-213
Temporal logic: Mathematical foundations
Gabbay, Dov M.
March 1992, 166 pages.
.
Status: distribution forbidden
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.
References to related material:
An Oxford University Press Book is available: Dov M. Gabbay,Mark Reynolds,Ian Hodkinson: Temporal Logic