# Temporal Logic

*First published Mon Nov 29, 1999; substantive revision Thu Dec 11, 2003*

The term Temporal Logic has been broadly used to cover all approaches to the representation of temporal information within a logical framework, and also more narrowly to refer specifically to the modal-logic type of approach introduced around 1960 by Arthur Prior under the name of Tense Logic and subsequently developed further by logicians and computer scientists.

Applications of Temporal Logic include its use as a formalism for clarifying philosophical issues about time, as a framework within which to define the semantics of temporal expressions in natural language, as a language for encoding temporal knowledge in artificial intelligence, and as a tool for handling the temporal aspects of the execution of computer programs.

- 1. Modal-logic approaches to temporal logic
- 2. Predicate-logic approaches to temporal logic
- 3. Philosophical issues
- 4. Applications
- Bibliography
- Other Internet Resources
- Related Entries

## 1. Modal-logic approaches to temporal logic

### 1.1 Tense Logic

Tense Logic was introduced by Arthur Prior (1957, 1967, 1969) as a result of an interest in the relationship between tense and modality attributed to the Megarian philosopher Diodorus Cronus (ca. 340-280 B.C.). For the the historical context leading up to the introduction of Tense Logic, as well as its subsequent developments, see Øhrstrøm and Hasle, 1995.The logical language of Tense Logic contains, in addition to the usual truth-functional operators, four modal operators with intended meanings as follows:

P "It has at some time been the case that …" F "It will at some time be the case that …" H "It has always been the case that …" G "It will always be the case that …"

P and F are known as the *weak tense operators*, while H and
G are known as the *strong tense operators*. The two pairs are
generally regarded as interdefinable by way of the equivalences

Pp ≡ ¬H¬p Fp ≡ ¬G¬p

On the basis of these intended meanings, Prior used the operators to build formulae expressing various philosophical theses about time, which might be taken as axioms of a formal system if so desired. Some examples of such formulae, with Prior's own glosses (from Prior 1967), are:

Gp→Fp "What will always be, will be" G(p→q)→(Gp→Gq) "If p will always imply q, then if p will always be the case, so will q" Fp→FFp "If it will be the case that p, it will be — in between — that it will be" ¬Fp→F¬Fp "If it will never be that p then it will be that it will never be that p"

Prior (1967) reports on the extensive early work on various systems of Tense Logic obtained by postulating different combination of axioms, and in particular he considered in some detail what light a logical treatment of time can throw on classic problems concerning time, necessity and existence; for example, "deterministic" arguments that have been advanced over the ages to the effect that "what will be, will necessarily be", corresponding to the modal tense-logical formula Fp→□Fp.

Of particular significance is the system of *Minimal Tense
Logic* K_{t}, which is generated by the four axioms

together with the two rules of temporal inference:

p→HFp "What is, has always been going to be" p→GPp "What is, will always have been" H(p→q)→(Hp→Hq) "Whatever always follows from what always has been, always has been" G(p→q)→(Gp→Gq) "Whatever always follows from what always will be, always will be"

and, of course, all the rules of ordinary Propositional Logic. The theorems of K

RH: From a proof of p, derive a proof of Hp RG: From a proof of p, derive a proof of Gp

_{t}express, essentially, those properties of the tense operators which do not depend on any specific assumptions about the temporal order. This characterisation is made more precise below.

Tense Logic is obtained by adding the tense operators to an existing
logic; above this was tacitly assumed to be the classical Propositional
Calculus. Other tense-logical systems are obtained by taking different
logical bases. Of obvious interest is tensed predicate logic, where the
tense operators are added to classical First-order Predicate Calculus.
This enables us to express important distinctions concerning the logic
of time and existence. For example, the statement *A philosopher
will be a king* can be interpreted in several different ways, such
as

The interpretation of such formulae is not unproblematic, however. The problem concerns the domain of quantification. For the second two formulae above to bear the interpretations given to them, it is necessary that the domain of quantification is always relative to a time: thus in the semantics it will be necessary to introduce a domain of quantification D(t) for each time t. But this can lead to problems if we want to establish relations between objects existing at different times, as for example in the statement "One of my friends is descended from a follower of William the Conqueror".

∃x(Philosopher(x) & F King(x)) Someone who is now a philosopher will be a king at some future time ∃xF(Philosopher(x) & King(x)) There now exists someone who will at some future time be both a philosopher and a king F∃x(Philosopher(x) & F King(x)) There will exist someone who is a philosopher and later will be a king F∃x(Philosopher(x) & King(x)) There will exist someone who is at the same time both a philosopher and a king

These problems are related to the so-called *Barcan formulae*
of modal logic, a temporal analogue of which is

F∃xp(x)→∃xFp(x) ("If there will be something that is p, then there is now something that will be p")

For this formula to be true, we require the "domain cumulation" principle, which says that the whole domain of quantification D(t) at time t is included in all the domains D(t′) for times t′ later than t. For more on this and related matters, see van Benthem, 1995, Section 7.

### 1.2 Extensions to Tense Logic

Soon after its introduction, the basic "PFGH" syntax of Tense Logic was extended in various ways, and such extensions have continued to this day. Some important examples are the following:
**The binary temporal operators S and U ("since" and
"until")**. These were introduced by Kamp (1968). The intended
meanings are

It is possible to define the one-place tense operators in terms of S and U as follows:

Spq "q has been true since a time when p was true" Upq "q will be true until a time when p is true"

Pp ≡ Sp(p¬p) Fp ≡ Up(p¬p)

The importance of the S and U operators is that they are expressively complete with respect to first-order temporal properties on continuous, strictly linear temporal orders (which is not true for the one-place operators on their own).

**Metric tense logic**. Prior introduced the notation
Fnp to mean "It will be the case the interval n hence that p". We do
not need a separate notation Pnp since we can write F(-n)p for "It was
the case the interval n ago that P". The case n=0 gives us the present
tense. We can define the general, non-metric operators by

Pp ≡ ∃n(n<0 & Fnp) Fp ≡ ∃n(n>0 & Fnp) Hp ≡ ∀n(n<0→Fnp) Gp ≡ ∀n(n>0→Fnp)

**The "next time" operator O**. This operator assumes
that the time series consists of a discrete sequence of atomic times.
The formula Op is then intended to mean that p is true at the
immediately succeeding time step. Given that time is discrete, it can
be defined in terms of the "until" operator U by

Op ≡ Up(p&¬p)

which says that p will be true at some future time, between which and the present time nothing is true. This can only mean the time immediately following the present in a discrete temporal order.

In discrete time, the future-tense operator F is related to the next-time operator by the equivalence

Fp ≡ Op OFp.Indeed, F can here be

*defined*as the least fixed point of the transformation which maps an arbitrary propositional operator X onto the operator λp.OpOXp.

One could similarly define a past-time version of O; but since the main usefulness of this particular operator has been in relation to the logic of computer programming, where one is mainly interested in execution sequences of programs extending into the future, this has not so often been done.

### 1.3 Semantics of Tense Logic

The standard model-theoretic semantics of Tense Logic is closely modelled on that of Modal Logic. A*temporal frame*consists of a set T of entities called times together with an ordering relation < on T. This defines the "flow of time" over which the meanings of the tense operators are to be defined. An interpretation of the tense-logical language assigns a truth value to each atomic formula at each time in the temporal frame. Given such an interpretation, the meanings of the weak tense operators can be defined using the rules

from which it follows that the meanings of the strong operators are given by

Pp is true at t if and only if p is true at some time t′ such that t′<t Fp is true at t if and only if p is true at some time t′ such that t<t′

Hp is true at t if and only if p is true at all times t′ such that t′<t Gp is true at t if and only if p is true at all times t′ such that t<t′

We can now provide a precise characterisation of system
K_{t} of Minimal Tense Logic. The theorems of K_{t} are
precisely those formulae which are true at all times under all
interpretations over all temporal frames.

Many tense-logical axioms have been suggested as expressing this or
that property of the flow of time, and the semantics gives us a precise
way of defining this correspondence between tense-logical formulae and
properties of temporal frames. A formula p is said to
*characterise* a set of frames F if

- p is true at all times under all interpretations over any frame in F.
- For any frame not in F, there is an interpretation which makes p false at some time.

_{t}characterises the class of all frames.

A first-order formula in < determines a class of frames, namely those in which the formula is true. A tense-logical formula p corresponds to a first-order formula q just so long as p characterises the class of frames for which q is true. Some well-known examples of such pairs of formulae are:

However, there are tense-logical formulae (such as GFp→FGp) which do not correspond to any first-order temporal frame properties, and there are first-order temporal frame properties (such as

Hp→Pp ∀t∃t′(t′<t) (unbounded in the past) Gp→Fp ∀t∃t′(t<t′) (unbounded in the future) Fp→FFp ∀t,t′(t<t′ → ∃t″(t<t″<t′)) (dense ordering) FFp→Fp ∀t,t′(∃t″(t<t″<t′) → t<t′) (transitive ordering) FPp → PppFp ∀t,t′,t″((t<t″ & t′<t″) → (t<t′ t=t′ t′<t)) (linear in the past) PFp → PppFp ∀t,t′,t″((t″<t & t″<t′) → (t<t′ t=t′ t′<t)) (linear in the future)

*irreflexivity*, expressed by ∀t¬(t<t)) which do not correspond to any tense-logical formula. For details, see van Benthem (1983).

## 2. Predicate-logic approaches to temporal logic

### 2.1 The method of temporal arguments

In this method, the temporal dimension is captured by augmenting each time-variable proposition or predicate with an extra argument-place, to be filled by an expression designating a time, as for exampleKill(Brutus,Caesar,44BC).If we introduce into the first-order language a binary infix predicate < denoting the temporal ordering relation "earlier than", and a constant "now" denoting the present moment, then the tense operators can be readily simulated by means of the following correspondences, which not surprisingly bear more than a passing resemblance to the formal semantics for Tense Logic given above. Where p(t) represents the result of introducing an extra temporal argument place to the time-variable predicates occurring in p, we have:

Before the advent of Tense Logic, the method of temporal arguments was the natural choice of formalism for the logical expression of temporal information.

Pp ∃t(t<now & p(t)) Fp ∃t(now<t & p(t)) Gp ∀t(t<now → p(t)) Hp ∀t(now<t → p(t))

### 2.2 Hybrid approaches

The reification of time instants implied by the method of temporal arguments may be regarded as philosophically suspect, instants being rather artificial constructs unsuited to playing a foundational role in temporal discourse. Following a suggestion of Prior (1968, Chapter XI), one might equate an instant with ‘the conjunction of all those propositions which would ordinarily be said to be true at that instant’. Instants are thus replaced by propositions which uniquely characterise them. A statement of the form "True(p,t)", saying that proposition p is true at instant t, can then be paraphrased as "□ (t→ p)", i.e., the instant-proposition t necessarily implies p.This kind of manoeuvre lies at the heart of hybrid temporal logics in which the standard apparatus of propositions and tense operators is supplemented by propositions which are true at unique instants, thereby effectively naming those instants without invoking philosophically dubious reification. This can give one some of the expressive power of a predicate-logic approach while retaining the modal character of the logic.

### 2.3 State and event-type reification

The method of temporal arguments encounters difficulties if it is desired to model*aspectual*distinctions between, for example, states, events and processes. Propositions reporting states (such as "Mary is asleep") have

*homogeneous*temporal incidence, in that they must hold over any subintervals of an interval over which they hold (e.g., if Mary is asleep from 1 o'clock to 6 o'clock then she is asleep from 1 o'clock to 2 o'clock, from 2 o'clock to 3 o'clock, and so on). By contrast, propositions reporting events (such as "John walks to the station") have inhomogeneous temporal incidence; more precisely, such a proposition is not true of

*any*proper subinterval of an interval of which it is true (e.g., if John walks to the station over the interval from 1 o'clock to a quarter past one, then it is not the case that he walks to the station over the interval from 1 o'clock to five past one — rather, over that interval he walks part of the way to the station).

The method of state and event-type reification was introduced to cater for distinctions of this kind. It is an approach that has been especially popular in Artificial Intelligence, where it is particularly associated with the name of James Allen, whose influential paper (Allen 1984) is often cited in this connection. In this approach, state and event types are denoted by terms in a first-order theory; their temporal incidence is expressed using relational predicates "Holds" and "Occurs", as for example,

Holds(Asleep(Mary),(1pm,6pm))where terms of the form (t,t′) denote time intervals in the obvious way.

Occurs(Walk-to(John,Station),(1pm,1.15pm))

The homogeneity of states and inhomogeneity of events is secured by axioms such as

∀s,i,i′(Holds(s,i) & In(i′,i) → Holds(s,i′))where "In" expresses the proper subinterval relation.

∀e,i,i′(Occurs(e,i) & In(i′,i) → ¬Occurs(e,i′))

### 2.4 Event-token reification

The method of event-token reification was proposed by Donald Davidson (1967) as a solution to the so-called "variable polyadicity" problem. The problem is to give a formal account of the validity of such inferences asThe key idea is that each event-forming predicate is endowed with an extra argument-place to be filled with a variable ranging over event-tokens, that is, particular dated occurrences. The inference above is then cast in logical form as

John saw Mary in London on Tuesday. Therefore, John saw Mary on Tuesday.

In this form, the inference does not require any additional logical apparatus over and above standard first-order predicate logic; on that basis, the validity of the inference is considered to be explained. This approach has also been used in a computational context in the Event Calculus of Kowalski and Sergot (1986).

∃e(See(John,Mary,e) & Place(e,London) & Time(e,Tuesday)), Therefore, ∃e(See(John,Mary,e) & Time(e,Tuesday)).

## 3. Philosophical issues

Prior's motivation for inventing Tense Logic was largely philosophical, his idea being that the precision and clarity afforded by a formal logical notation was indispensible for the careful formulation and resolution of philosophical issues concerning time. See the article on Arthur Prior for a discussion of some of these.### 3.1 Realist vs reductionist approaches to tense

The rivalry between the modal and first-order approaches to formalising the logic of time reflects an important set of underlying philosophical issues related to the work of McTaggart. This work is especially well-known, in the context of temporal logic, for introducing the distinction between the "A-series" and the "B-series". By the "A-series" is meant, essentially, the characterisation of events as Past, Present, or Future. By contrast, the "B-series" involves their characterisation as relatively "Earlier" or "Later". A-series representations of time inescapably single out some particular moment as present; of course, at different times, different moments are present — a circumstance which, followed to what appeared to be its logical conclusion, led McTaggart to assert that time itself was unreal (see Mellor, 1981). B-series representations have no place for a concept of the present, instead taking the form of a synoptic view of all time and the (timeless) interrelations between its parts.

There is a clear affinity between the A-series and the modal approach and between the B-series and the first-order approach. In the terminology of Massey (1969), adherents of the former approach are called "tensers" while adherents of the latter are called "detensers". This issue is related in turn to the question of how seriously to take the representation of space-time as a single four-dimensional entity in which the four dimensions are at least in some respects on a similar footing. In view of the Theory of Relativity, it can be argued that this issue is not so much a matter for Philosophy as for Physics.

### 3.2 Determinism vs non-determinism

The choice of flow of time can be of philosophical significance. For
example, one way of capturing the distinction between deterministic and
non-deterministic theories is to model the former using a strictly
linear flow of time, and the latter with a temporal structure which
allows branching into the future. If we adopt the latter approach, then
it is helpful in describing the semantics of tense and other operators
to introduce the idea of a *history*, which is a maximal
linearly-ordered set of instants. The branching future model will then
stipulate that for any two histories there is an instant such that both
histories share all the times up to and including that instant, but do
not share any times after it. For each history containing a given
instant, the times in that history which are later than the instant
constitute a "possible future" for that instant.

In branching time semantics it is natural to evaluate formulae with respect to an instant and a history, rather than just an instant. With respect to the pair (h,t), we might interpret "Fp" to be true so long as "p" is true at some time in the future of t as determined by the history h. A separate operator ◊ can be introduced to allow, in effect, quantification over histories: "◊p" is true at (h,t) so long as there is some history h’ such that "p" is true at (h’,t). Then "◊Fp" says that "p" holds in some possible future, and "□Fp" (where "□" is the strong modal operator dual to "◊") says that "p" is inevitable (i.e., holds in all possible futures). Prior calls this kind of interpretation "Ockhamist".

Another interpretation (called "Peircean" by Prior) takes "Fp" to be
equivalent to the Ockhamist "□Fp", i.e., "p" is true at some time
in *every* possible future. Under this interpretation there is
no formula equivalent to the Ockhamist "Fp"; hence Peircean tense logic
is a proper fragment of Ockhamist tense logic. It was favoured by Prior
on the grounds that future contingent propositions really do lack truth
value: only if a future-tense proposition is inevitable (all possible
futures) or impossible (no possible futures) can we ascribe a truth
value to it now.

For Prior's discussion of these issues, see Prior 1967, Chapter VII. Further discussion can be found in Øhrstrøm, P. and Hasle, P., 1995, chapters 2.6 and 3.2.

## 4. Applications of Temporal Logic

### 4.1 Applications to natural language

Prior (1967) lists amongst the precursors of Tense Logic Hans Reichenbach's (1947) analysis of the tenses of English, according to which the function of each tense is to specify the temporal relationships amongst a set of three times related to the utterance, namely S, the speech time, R, the reference time, and E, the event time. In this way Reichenbach was neatly able to distinguish between the simple past "I saw John", for which R=E<S, and the present perfect "I have seen John", for which E<R=S, the former statement referring to a past time coincident with the event of my seeing John, the latter referring to the present time, relative to which my seeing John is past.
Prior notes that Reichenbach's analysis is inadequate to account for
the full range of tense usage in natural language. Subsequently much
work has been done to refine the analysis, not only of tenses but also
other temporal expressions in language such as the temporal
prepositions and connectives ("before", "after", "since", "during",
"until"), using the many varieties of temporal logic. For some
examples, see Dowty (1979), Galton (1984), Taylor (1985), Richards
*et al.* (1989).

### 4.2 Applications in artificial intelligence

We have already mentioned the work of Allen (1984), which is concerned with finding a general framework adequate for all the temporal representations required by AI programs. The Event Calculus of Kowalski and Sergot (1986) is pursued more specifically within the framework of logic programming, but is otherwise similarly general in character. A useful survey of issues involving time and temporal reasoning in AI is Galton (1995).
Much of the work on temporal reasoning in AI has been closely tied
up with the notorious *frame problem*, which arises from the
necessity for any automated reasoner to know, or be able to deduce, not
only those properties of the world which *do* change as the
result of any event or action, but also those properties which do
*not* change. In everyday life, we normally handle such facts
fluently without consciously adverting to them: we take for granted
without thinking about it, for example, that the colour of a car does
not normally change when one changes gear. The frame problem is
concerned with how to formalise the logic of actions and events in such
a way that indefinitely many inferences of this kind are made available
without our having to encode them all explicitly. A seminal work in
this area is McCarthy and Hayes (1969). A useful recent reference for
the frame problem is Shanahan, 1997.

### 4.3 Applications in computer science

Following Pnueli (1977), the modal style of Temporal Logic has found extensive application in the area of Computer Science concerned with the specification and verification of programs, especially concurrent programs in which the computation is performed by two or more processors working in parallel. In order to ensure correct behaviour of such a program it is necessary to specify the way in which the actions of the various processors are interrelated. The relative timing of the actions must be carefully co-ordinated so as to ensure that integrity of the information shared amongst the processors is maintained. Amongst the key notions here is the distinction between "liveness" properties of the tense-logical form Fp, which ensure that desirable states will obtain in the course of the computation, and "safety" properties of the form Gp, which ensure that undesirable states will never obtain.Non-determinism is an important issue in computer science applications, and hence much use has been made of branching time models. Two important such systems are CTL (Computation Tree Logic) and a more expressive system CTL*; these correspond very nearly to the Ockhamist and Peircean semantics discussed above.

Further information may be found in Galton (1987), Goldblatt (1987), Kroger (1987), Bolc and Szalas (1995).

## Bibliography

- Allen, J. F., 1984,"Towards a general theory of action and time",
*Artificial Intelligence*, volume 23, pages 123-154. - van Benthem, J., 1983,
*The Logic of Time*, Dordrecht, Boston and London: Kluwer Academic Publishers, first edition (second edition, 1991). - van Benthem, J., 1995, "Temporal Logic", in D. M. Gabbay, C. J.
Hogger, and J. A. Robinson,
*Handbook of Logic in Artificial Intelligence and Logic Programming*, Volume 4, Oxford: Clarendon Press, pages 241-350. - L. Bolc and A. Szalas (eds.), 1995,
*Time and Logic: A Computational Approach*, London: UCL Press. - Davidson, D., 1967, "The Logical Form of Action Sentences", in N.
Rescher (ed.),
*The Logic of Decision and Action*, University of Pittsburgh Press, 1967, pages 81-95. Reprinted in D. Davidson,*Essays on Actions and Events*, Oxford: Clarendon Press, 1990, pages 105-122. - Dowty, D., 1979,
*Word Meaning and Montague Grammar*, Dordrecht: D. Reidel. - Gabbay, D. M., Hodkinson, I., and Reynolds, M., 1994,
*Temporal Logic: Mathematical Foundations and Computational Aspects*, Volume 1,. Oxford: Clarendon Press. - Galton, A. P., 1984,
*The Logic of Aspect*, Oxford: Clarendon Press. - Galton, A. P., 1987,
*Temporal Logics and their Applications*, London: Academic Press. - Galton, A. P., 1995, "Time and Change for AI", in D. M. Gabbay, C.
J. Hogger, and J. A. Robinson,
*Handbook of Logic in Artificial Intelligence and Logic Programming*, Volume 4, Oxford: Clarendon Press, pages 175-240. - Goldblatt, R., 1987,
*Logics of Time and Computation*, Center for the Study of Language and Information, CSLI Lecture Notes 7. - Kamp, J. A. W., 1968.
*Tense Logic and the Theory of Linear Order*, Ph.D. thesis, University of California, Los Angeles. - Kowalski, R. A. and Sergot, M. J., 1986, "A Logic-Based Calculus of
Events",
*New Generation Computing*, volume 4, pages 67-95. - Kroger, F., 1987, "Temporal Logic of Programs", Springer-Verlag.
- Massey, G., 1969, "Tense Logic! Why Bother?",
*Noûs*, volume 3, pages 17-32. - McCarthy, J. and Hayes, P. J., 1969, "Some Philosophical Problems
from the Standpoint of Artificial Intelligence", in D. Michie and B.
Meltzer (eds.),
*Machine Intelligence 4*, Edinburgh University Press, pages 463-502. - Mellor, D. H., 1981,
*Real Time*, Cambridge: Cambridge University Press. (Chapter 6 reprinted with revisions as "The Unreality of Tense" in R. Le Poidevin and M. MacBeath (eds.),*The Philosophy of Time*, Oxford University Press, 1993.) - Øhrstrøm, P. and Hasle, P., 1995,
*Temporal Logic: From Ancient Ideas to Artificial Intelligence*, Dordrecht, Boston and London: Kluwer Academic Publishers. - Pnueli, A., 1977, "The temporal logic of programs",
*Proceedings of the 18th IEEE Symposium on Foundations of Computer Science*, pages 46-67. - Prior, A. N., 1957,
*Time and Modality*, Oxford: Clarendon Press. - Prior, A. N., 1967,
*Past, Present and Future*, Oxford: Clarendon Press. - Prior, A. N., 1969,
*Papers on Time and Tense*, Oxford: Clarendon Press. - Reichenbach, H., 1947,
*Elements of Symbolic Logic*, New York: Macmillan - Rescher, N. and Urquhart, A., 1971,
*Temporal Logic*, Springer-Verlag. - Richards, B., Bethke, I., van der Does, J., and Oberlander, J.,
1989,
*Temporal Representation and Inference*, London: Academic Press. - Shanahan, M., 1997,
*Solving the Frame Problem*, Cambridge MA and London: The MIT Press. - Taylor, B., 1985,
*Modes of Occurrence*, Aristotelian Society Series, Volume 2, Oxford: Basil Blackwell.

## Other Internet Resources

- Foundations of Temporal Logic — The WWW-site for Prior-studies, by Per Hasle and Peter Øhrstrøm.