Temporal Logic

First published Mon Nov 29, 1999; substantive revision Wed May 20, 2015

The term Temporal Logic has been broadly used to cover all approaches to representation and reasoning about time and 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 many 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 specification, formal analysis, and verification of the executions of computer programs and systems.

Here we provide a broadly representative, yet concise and inevitably incomplete, overview of the rich variety of temporal models and logics introduced and studied over the past 50 years.

1. Temporal reasoning from antiquity to modern days

Discussion of temporality and reasoning about time goes back to antiquity and examples can be found even in the Bible (Boyd 2014). Some of Zeno’s paradoxical arguments refer to the nature of time and the question of infinite divisibility of time intervals. Perhaps the earliest scientific reference on temporal reasoning, however, is Aristotle’s argument in On Interpretation, Ch. 9, that future contingents, i.e., statements about possible future events which may or may not occur, such as “There will be a sea-fight tomorrow”, should not be ascribed definite truth values at the present time. A few decades later the philosopher Diodorus Cronus (ca 340–280 BC) from the Megarian school demonstrated the problem of future contingents in his famous Master Argument where, inter alia, he defined “possible” as “what is or will ever be” and “necessary” as “what is and will always be”. For details, see Rescher and Urquhart (1971, Chapter XVII) and the entry on future contingents.

Philosophical discussion on temporality, truth, free will, determinism, and how they are related, continued during the Middle ages. William of Ockham (c. 1287–1347) argued that propositions about the contingent future cannot be known by humans as true or false because only God knows their truth value now. However, he argued that humans still have some freedom of choice amongst different possible futures, thus suggesting the idea of a future-branching model of time with many possible time-lines (histories), truth of propositions being relativised to a possible actual history; this model of time is now often called Ockhamist. Later, several philosophers and logicians, including C. S. Peirce, raised and analysed problems relating temporality with non-determinism, historical necessity, free will, God’s will and knowledge, etc., proposing various different solutions. For a more recent philosophical discussion on free will vs. determinism see Belnap et al. (2001).

From the early 1950s Arthur Prior set out to analyse and formalise such arguments, leading him, inter alia, to the invention of formal Temporal Logic[1], several versions of which are discussed below. Prior’s seminal work, partly influenced by important precursors such as J. Findlay, H. Reichenbach and J. Łukasiewicz, initiated the modern era of temporal logical reasoning, with numerous important applications not only to philosophy, but also to computer science, artificial intelligence, and linguistics, briefly discussed below in Section 10.

Time is not only a philosophical, but also a fundamental physical concept, and as such it has been studied and analysed throughout the history of science. Early physical theories, culminating with Newton’s classical mechanics, presuppose an absolute concept of time, independent from space, matter, and all other fundamental physical concepts. Opposed to this, Leibniz advocated a relational view according to which time is dependent on processes and events, but such a view did not find expression in physics until the relativist views of the early 20th century, which put time in a mathematically involved relationship with space, modelled by Minkowski’s four-dimensional space-time manifold, and with matter, captured by Einstein’s relativity theory. We will not discuss physical theories of time further here but we should mention Rescher and Urquhart (1971, Chapter XVI), where space-time reasoning and dimensionality of time are discussed, and Goldblatt (1980), where the Diodorean modal logic of Minkowskian spacetime was studied and proved to be exactly the modal logic S4.2 and a number of related questions, some of which still open, were raised.

For further reading on the history of temporal reasoning and logics see Øhrstrøm and Hasle (1995).

2. Formal models of time

The ontological nature and properties of time are fundamental philosophical issues. Distinct alternatives along several dimensions have been debated since antiquity and choices amongst these alternatives are crucial for the philosophical discourse on the nature of time; is time, for example, discrete or continuous; instant-based or interval-based; bounded or unbounded; deterministic or not; linear or (forward) branching; circular, etc.? We briefly discuss some of these alternatives below, and return to them again in the formal context of temporal logics.

2.1 Instant-based models of the flow of time

In instant-based models of time the primitive temporal entities are time instants and the basic relationship between them (besides equality) is precedence. Thus, the flow of time is represented as a set of time instants with a binary relation of precedence on it: \(\left\langle T, \prec \right\rangle.\) There are some basic properties which can naturally be imposed on instant-based flows of time. It is usually required to be a strict partial ordering, that is, an irreflexive and transitive relation. Sometimes, however, it is assumed reflexive and then the antisymmetry condition is added. Two main types of such models are usually considered: linear orderings, reflecting the idea that the time flow is a succession of instants, and forward branching partial orderings, representing the idea that past is determined and therefore linear, while the future can be undetermined, branching into many possible time lines. Some further basic properties which an instant-based model \(\left\langle T, \prec \right\rangle\) may or may not have can be expressed with first-order sentences as follows (where \(\preceq\) is an abbreviation of \(x\prec y \lor x=y\)):

  • reflexivity: \(\forall x (x\prec x);\) respectively irreflexivity: \(\forall x\lnot (x\prec x);\)
  • transitivity: \(\forall x\forall y\forall z(x\prec y\wedge y\prec z\rightarrow x\prec z);\)
  • anti-symmetry:  \(\forall x\forall y(x\prec y\wedge y\prec x\rightarrow x=y),\)
  • trichotomy (connectedness): \(\forall x\forall y(x=y\vee x\prec y\vee y\prec x);\)
  • density (between every two precedence-related instants there is an instant): \(\forall x\forall y(x\prec y\rightarrow \exists z(x\prec z\wedge z\prec y));\)
  • no beginning: \(\forall x\exists y(y\prec x);\)   no end: \(\forall x\exists y(x\prec y);\)
  • every instant has an immediate successor: \(\forall x\exists y(x\prec y\wedge \forall z(x\prec z\rightarrow y\preceq z))\) and, likewise, every instant has an immediate predecessor: \(\forall x\exists y(y\prec x \wedge \forall z(z\prec x\rightarrow z\preceq y));\)
  • forward discreteness (every instant with a successor has an immediate successor): \(\forall x\exists y(x\prec y\rightarrow \exists y(x\prec y\wedge \forall z(x\prec z\rightarrow y\preceq z)));\)
  • backward discreteness (every instant with a predecessor has an immediate predecessor): \(\forall x\exists y(y\prec x\rightarrow \exists y(y\prec x\wedge \forall z(z\prec x\rightarrow z\preceq y))).\)

Some natural and important properties of time flows cannot be expressed with first-order sentences. For example, one cannot say in first-order logic that a linear time flow is well-ordered, meaning that every strictly descending sequence of time instants must be finite. Equivalently, well-ordering means that every non-empty set of time instants has a \(\prec\)-least element. An example is the ordered set of natural numbers \(\left\langle \mathbf{N,<}\right\rangle;\) non- examples are the integers \(\left\langle \mathbf{Z,<}\right\rangle\) (take the set of negative integers), the positive rationals \(\left\langle \mathbf{Q^{+},<}\right\rangle\) or the positive reals \(\left\langle \mathbf{R^{+},<}\right\rangle.\) Neither can Dedekind completeness be expressed, stating that every non-empty set of instants which has an upper bound has a least upper bound. Examples are the orderings of the natural numbers, integers or reals; a non-example is the ordered set of rationals: consider the set of all rationals whose square is less than 2. To express these properties, one needs a monadic second order-logic involving quantification over sets. As shown further, however, some such properties can be expressed in suitably expressive propositional temporal logics.

2.2 Interval/period based models of time

Instant-based models are often not suitable for reasoning about real-world events with duration, which are better modeled if the underlying temporal ontology uses time intervals, rather than instants, as the primitive entities. For instance, statements like “Last night Alice cried a lot while writing the letter, and then she calmed down”, “Always after dinner the old man took a walk followed by a long bath”, “The construction of the present St Peter’s Basilica took over 120 years”, or “Bill never drinks his morning coffee in less than 2 minutes” naturally require interval-based models of time to be adequately modelled and evaluated.

Interval-based temporal models are ontologically richer than instant-based ones, as there are many more possible relationships between time intervals than between time instants. For instance, a natural interval-based model of time \(\mathcal{T}\) can include the relations precedence \(\prec,\) inclusion \(\sqsubseteq\) and overlap \(O\) between intervals over some time flow \(T:\) formally, \(\mathcal{T}= \left\langle T,\prec,\sqsubseteq, O \right\rangle.\) Some natural basic properties of such interval-based relations and models include:

  • reflexivity of \(\sqsubseteq:\) \(\forall x(x\sqsubseteq x),\)
  • anti-symmetry of \(\sqsubseteq:\)  \(\forall x\forall y(x\sqsubseteq y\wedge y\sqsubseteq x\rightarrow x=y),\)
  • atomicity of \(\sqsubseteq\) (for discrete time): \(\forall x\exists y(y\sqsubseteq x\wedge \forall z(z\sqsubseteq y\rightarrow z=y)).\)
  • downward monotonicity of \(\prec\) wrt \(\sqsubseteq:\) \(\forall x\forall y\forall z(x\prec y\wedge z\sqsubseteq x\rightarrow z\prec y).\)
  • symmetry of \(O:\) \(\forall x\forall y(xOy\rightarrow yOx)\)
  • overlapping intervals intersect in a subinterval:
    \(\forall x\forall y (xOy \rightarrow \exists z( z \sqsubseteq x \land z \sqsubseteq y \land \forall u (( u \sqsubseteq x \land u \sqsubseteq y) \to u \sqsubseteq z))).\)
  • monotonicity of \(\sqsubseteq\) wrt \(O:\) \(\forall x\forall y \forall z(x \sqsubseteq y \land xOz \rightarrow (z \sqsubseteq y \lor zOy)).\)

This is only a small sample of such properties, for which the truth conditions can be precisely defined. Given an abstract structure defined by such a set of relations and their properties, the question arises whether it can be represented by means of a concrete interval model over linear time. Answers are provided by various representation theorems, see e.g., van Benthem (1983), Ladkin (1987), and Venema (1990).

In an influential early work on the formal study of interval-based temporal ontology and reasoning in AI, Allen (1983) considered the family of all 13 binary relations arising between two intervals in a given linear order, subsequently called Allen relations, displayed in Table 1. These 13 relations are mutually exclusive and jointly exhaustive, meaning that exactly one of them holds between any given pair of strict intervals (i.e., excluding point-intervals). They turn out to be definable in terms of a couple of them, viz. ‘meets’ and ‘met-by’ (Allen 1983).

2.3 Instant vs interval based models of time

The nature of time and, in particular, the choice between instants and intervals as the primary objects of temporal ontology, has been a hotly debated philosophical theme. The roots of interval-based temporal reasoning can be traced back to Zeno and Aristotle (Øhrstrøm and Hasle 1995). Apparently, Zeno himself noticed that some of his paradoxes do not arise in an interval-based setting, for example the flying arrow paradox (“if at each instant the flying arrow stands still, how is movement possible?”) and the dividing instant dilemma (“if the light is on and it is turned off, what is its state at the instant between the two events?”). Of course, the two types of temporal ontologies are closely related and technically reducible to each other: on the one hand, time intervals can be determined by pairs of time instants (beginning–end); on the other hand, a time instant can be construed as a degenerate ‘point interval’, whose endpoints coincide. See van Benthem (1983) for a detailed comparative discussion of both approaches.

Interval relationsAllen’s notation\(\textsf{HS}\) notation
┣━━┫ equals \(\{=\}\)
├──┤ ┣┫ before \(\{\lt\}\) / after \(\{\gt\}\) \(\langle L\rangle\:/\:\langle\overline{L}\rangle\) Later
├──╊┫ meets \(\{m\}\) / met-by} \(\{mi\}\) \(\langle A\rangle\:/\:\langle\overline{A}\rangle\) After
├─╊┿━┫ overlaps \(\{o\}\) / overlapped-by \(\{oi\}\) \(\langle O\rangle\:/\:\langle\overline{O}\rangle\) Overlaps
├─╊┫ finished-by \(\{fi\}\) / finishes \(\{f\}\) \(\langle E\rangle\:/\:\langle\overline{E}\rangle\) Ends
├╊╉┤ contains \(\{di\}\) / during \(\{d\}\) \(\langle D\rangle\:/\:\langle\overline{D}\rangle\) During
┣╉─┤ started-by \(\{si\}\) / starts \(\{s\}\) \(\langle B\rangle\:/\:\langle\overline{B}\rangle\) Begins

Table 1: Allen relations between pairs of intervals and Halpern-Shoham modal operators on them.

Other models of time have been studied, too, including two-sorted, point-interval models (Balbiani et al. 2011), models of time granularity, metric and layered temporal models (Montanari 1996). See also the SEP entry on time.

3. Prior’s Basic Tense Logic TL

As noted above, 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 indispensable for the careful formulation and resolution of philosophical issues concerning time. Initially motivated by problems concerning the relationship between tense and modality raised by the Master Argument of Diodorus Cronus, Arthur Prior introduced and analysed in detail over more than a decade several versions of Tense Logic (Prior 1957; 1967; 1969). He did not subscribe to any particular choice, but rather held the modern view that “The logician must be like a lawyer … in the sense that he is there to provide the metaphysician, perhaps even the physicist, the tense-logic he wants, provided that it be consistent”.

3.1 Prior’s tense operators

The basic logical language of Prior’s Tense Logic TL contains, in addition to the usual propositional (truth-functional) operators, four temporal 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 …”

Thus, “\(GP\)(Prior invents Tense Logic)” translates as “It will always be the case that it has some time been the case that Prior invents Tense Logic”.

\(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 interdefinable by means of the equivalences

\[ P\varphi \equiv \neg H\neg \varphi, H\varphi \equiv \neg P\neg \varphi, F\varphi \equiv \neg G\neg \varphi, G\varphi \equiv \neg F\neg \varphi. \]

Formally, the set of formulae of TL can be recursively defined by: \[\varphi =p\mid \bot \mid \lnot \varphi \mid \varphi \lor \psi \mid G\varphi \mid H\varphi\] The other classical connectives \(\wedge,\to, \leftrightarrow\) are defined in terms of these as usual. Besides, we can define \(A\varphi =H\varphi \wedge \varphi \wedge G\varphi\) and, dually, \(E\varphi =P\varphi \vee \varphi \vee F\varphi,\) which on linearly ordered time flows mean always and sometime, respectively.

Various tenses in natural language can be expressed, at least approximately, in TL. For example:

  • \(P\varphi\) can corresponds both to present perfect (“\(\varphi\) has been the case”) and to past simple (“\(\varphi\) was the case”).
  • \(PP\varphi\) corresponds to “\(\varphi\) had been the case”,
  • \(FP\varphi\) corresponds to “\(\varphi\) will have been the case”,
  • \(PF\varphi\) corresponds to “\(\varphi\) was going to be the case” or “\(\varphi\) would be the case”,
  • \(PFP\varphi\) corresponds to “\(\varphi\) would have been the case”.

Hamblin and Prior identified 15 different such tenses that can be expressed in TL over linear flows of time, see (Prior, 1967). However, Prior’s operators are not very suitable for expressing progressive aspects of tenses. For instance, in addition to the examples given at the end of Section 2.2, sentences like “Bill was drinking his tea when the postman came”, “Bill always drinks his tea while reading the morning paper”, or “For seven hours the plane will be flying with a supersonic average speed” cannot be naturally captured in Prior’s tense logic TL. Arguably, interval-based logic is a more natural framework for that. For details, see Kuhn and Portner (2006) and the entry on tense and aspect.

3.2 Semantics of TL

Prior proposed, albeit informally, several different semantics for TL. The simplest one was essentially a possible worlds semantics in the style of the Kripke semantics for modal logic, given in instant-based temporal precedence models, hereafter called temporal frames. A temporal frame \(\mathcal{T}= \left\langle T, \prec \right\rangle\) defines the flow of time over which the meanings of the tense operators are to be defined. Note that, so far, no conditions like transitivity or irreflexivity on the “precedence” relation \(\prec\) are imposed.

A temporal model for a set of atomic propositions \(PROP\) is a triple \(\mathcal{M}= \left\langle T, \prec, V \right\rangle,\) where \(\left\langle T, \prec \right\rangle\) is a temporal frame and \(V\) is a valuation assigning to every \(p\in{PROP}\) a set of time instants \(V(p) \subseteq T\) at which \(p\) is declared true. Equivalently, an interpretation of \(PROP\) in \(\mathcal{T}\) is a mapping \(I: T\times{PROP}\to \{true,false\}\) which assigns a truth value to each atomic proposition at each time instant in the temporal frame. The truth of a formula of TL at a given time instant \(t\) in a given temporal model \(\mathcal{M}\) is defined inductively as follows:

\[\begin{align} \mathcal{M},t \models p &\text{ iff } t \in V(p), \text{ for } p \in {PROP}; \\ \mathcal{M},t \models \neg\psi &\text{ iff it is not the case that } \mathcal{M},t \models\psi; \\ \mathcal{M},t \models \varphi \vee \psi &\text{ iff } \mathcal{M},t \models\varphi \text{ or } \mathcal{M},t \models\psi; \\ \mathcal{M},t \models H\varphi &\text{ iff } \mathcal{M},t' \models \varphi \text{ for all time instants } t' \text{ such that } t'\prec t; \\ \mathcal{M},t \models G\varphi &\text{ iff } \mathcal{M},t' \models \varphi \text{ for all time instants } t' \text{ such that } t\prec t'. \end{align}\]

A formula \(\varphi\) of TL is valid, denoted \(\models \varphi,\) if it is true at all time instants in all temporal models; a formula \(\varphi\) is satisfiable if it is true at some time instant in some temporal model.

3.3 Standard translation of TL into first-order logic

The language and semantics of TL can be translated to classical first-order logic as follows. Suppose the set of atomic propositions of TL is \({PROP}=\left\{p_{0},p_{1},...\right\}.\) Let \(L_{1}\) be a first-order language with \(=,\) a binary predicate symbol \(R,\) and a denumerable set of unary predicate symbols \(\mathcal{P}=\left\{P_{0},P_{1},...\right\}.\)

The standard translation (see e.g. van Benthem 1983) \(ST\) of TL into \(L_{1}\) is now defined as follows, where \(\theta[y/x]\) is the result of substituting \(y\) for all free occurrences of \(x\) in \(\theta:\)

\[\begin{align} ST(p_{i}) &=P_{i}(x); \\ ST(\bot ) &=\bot; \\ ST(\varphi \lor \psi) &=ST(\varphi)\lor ST(\psi); \\ ST(G\varphi ) &=\forall y(xRy\rightarrow ST(\varphi)[y/x]), \text{ where } y \text{ is a fresh variable;} \\ ST(H\varphi ) &=\forall y(yRx\rightarrow ST(\varphi)[y/x]), \text{ where } y \text{ is a fresh variable.} \end{align}\]

It then follows that

\[\begin{align} ST(F\varphi)&=\exists y(xRy\wedge ST(\varphi )[y/x]), \\ ST(P\varphi)&=\exists y(yRx\wedge ST(\varphi )[y/x]). \end{align}\]

Example:
\(ST(Gp_{1}\lor FHp_{2})=\forall y(xRy\rightarrow P_{1}y)\lor \exists y(xRy\wedge \forall z(zRy\rightarrow P_{2}z)).\)

Now, every temporal model \(\mathcal{M}=\left\langle T,\prec ,V\right\rangle\) can be regarded as an \(L_{1}\)-model by interpreting \(R\) as \(\prec\) and each \(P_{i}\) as \(V(p_{i}).\) Then:

\[\begin{align} \mathcal{M},t \models \varphi &\text{ iff } \mathcal{M}\models ST(\varphi)[x:=t], \\ \mathcal{M} \models \varphi &\text{ iff } \mathcal{M}\models \forall x ST(\varphi). \end{align}\]

With a little extra care to re-use individual variables, TL can be translated in the two-variable fragment FO\(^{2}\) of first-order logic, which eventually implies decidability of the validity in TL. For instance, the example above can be equivalently re-written as

\[ST(Gp_{1}\lor FHp_{2})=\forall y(xRy\rightarrow P_{1}y)\lor \exists y(xRy\wedge \forall x(xRy\rightarrow P_{2}x)).\]

If the unary predicate symbols from \(\mathcal{P}\) are regarded as predicate variables, that yields a second-order language \(L_{2}.\) Then, every temporal frame can be regarded as an \(L_{2}\)-model, where the predicate variables represent the valuation of the respective atomic propositions. Let \(\forall \overline{P}\phi \) denote the universal closure of an \(L_{2}\)-formula \(\phi\) over all predicate variables occurring in it. Then for any TL formula \(\varphi\) and temporal frame \(\mathcal{T}:\) \[ \mathcal{T}\models \varphi \text{ iff }\mathcal{T}\models \forall \overline{P}\forall x ST(\varphi). \]

Therefore,

\[ \models \varphi \text{ iff }\models \forall \overline{P}\forall x ST(\varphi). \]

Thus, validity of a temporal formula in a model is a first-order property, while validity in a frame is a second-order property.

A temporal formula \(\varphi\) defines the class of temporal frames in which it is valid. Likewise, a first-order sentence in \(\prec\) and \(=\) defines the class of temporal frames in which it is true. For instance, as we noted earlier, \(\forall x\forall y (x=y \vee x\prec y\vee y\prec x)\) defines the class of frames with connected precedence relation \(\prec.\) A temporal formula \(\varphi\) is said to correspond to a first-order sentence \(\theta\) if \(\varphi\) defines the same class of frames which \(\theta\) defines. As we will see later, many but not all first-order definable properties of temporal frames are definable by temporal formulae and, vice versa, many but not all properties of temporal frames that are definable by temporal formulae are first-order definable. Thus, a non-trivial correspondence between temporal logic and first-order logic as alternative languages for describing properties of time flows emerges. This correspondence, based on the equivalences above, is at the heart of the correspondence theory between modal and classical logic, which offers a systematic treatment of various aspects of temporal logic such as expressiveness, definability, and model theory with the tools and techniques of classical logic. For further detail see Rescher and Urquhart (1971, Chapter XI), van Benthem (1983; 1995), Blackburn et al. (2006) and the entry on modal logic.

3.4 TL vs first-order logic and McTaggart’s time series

The relationship between different approaches to formalising the logic of time is of some relevance to philosophical questions concerning the nature of time. Certainly, in the early days of temporal logic the modal approach represented by Prior’s Tense Logic and its offshoots was perceived as a rival to more conventional approaches using first-order logic. This rivalry 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 “tensers”, while adherents of the latter are “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, this is arguably a matter for Physics rather than Philosophy.

3.5 Axiomatic system \(\mathbf{K}_{t}\) for TL

Like every formal logical system, temporal logic has two major aspects, semantic and deductive. Here we will present briefly the simplest types of deductive systems, viz. axiomatic systems, for some of the most important systems of temporal logics.

The minimal temporal logic \(\mathbf{K}_{t}\) axiomatizing all valid formulae of TL, was probably first proposed by Lemmon (see Rescher and Urquhart 1971, Chapter VI), following earlier systems proposed by Hamblin and Prior. It extends the classical propositional logic CL with the following axiom schemata:

  • \((K_G)\) \(G(\varphi \rightarrow \psi)\rightarrow (G\varphi \rightarrow G\psi),\)
  • “Whatever will always follow from what always will be, always will be”
  • \((K_H)\) \(H(\varphi \rightarrow \psi)\rightarrow (H\varphi \rightarrow H\psi),\)
  • “Whatever has always followed from what always has been, always has been”
  • (GP) \(\varphi \rightarrow GP\varphi,\)
  • “What is, will always have been”
  • (HF) \(\varphi \rightarrow HF\varphi,\)
  • “What is, has always been going to be”

and the following rules of inference, where \(\vdash\) means, as usual, “derived”:

  • (NEC\(_G\)) If \(\vdash \varphi\) then \(\vdash G\varphi\)
  • (NEG\(_H\)) If \(\vdash \varphi\) then \(\vdash H\varphi\)

added to the classical Modus Ponens: if \(\vdash \varphi\) and \(\vdash \varphi \rightarrow \psi\) then \(\vdash \psi.\)

The axioms (GP) and (HF) technically say that the temporal operators \(H\) and \(G\) correspond to mutually inverse temporal relations.

The axiomatic system \(\mathbf{K}_{t}\) is sound and complete for validity in TL, in the sense that it can derive all valid formulae of TL and only them. For a proof, see e.g., Rescher and Urquhart 1971 and Goldblatt 1987. Thus, the theorems of \(\mathbf{K}_{t}\) express those properties of the tense operators which do not depend on any specific assumptions about the temporal precedence relation.

3.6 Expressing temporal properties in TL and extensions of \(\mathbf{K}_{t}\)

3.6.1 Expressing some temporal properties in TL

We say that a temporal formula expresses a property \(\mathcal{P}\) of temporal frames if it defines the class of temporal frames satisfying the property \(\mathcal{P}.\)

Formulae from TL can express many natural properties of the flow of time. Taken as additional axioms, these would express various philosophical or ontological assumptions about time. Here are some important examples of correspondence between TL formulae and properties of temporal frames (recall that \(E p = Pp \vee p \vee Fp\)):

(REF) any of \(G\varphi \rightarrow \varphi,\) \(H\varphi \rightarrow \varphi,\) \(\varphi \rightarrow F\varphi,\) \(\varphi \rightarrow P\varphi\)
(reflexivity of \(\prec\))
(TRAN) any of \(Gp \rightarrow GGp,\) \(Hp \rightarrow HHp,\) \(FFp \rightarrow Fp,\) \(PPp \rightarrow Pp\)
(transitivity of \(\prec\))
(BEG) \(H\bot \vee PH\bot\)
(time has a beginning (assuming irreflexivity))
(NOBEG) \(P\top\)  or  \(Hp\rightarrow Pp\)
(time has no beginning)
(NOEND) \(F\top\)  or  \(Gp\rightarrow Fp\)
(time has no end)
(LIN-F) \( PFp \rightarrow Ep\)
(linearity in the future, meaning \(\forall {t}, t', t''((t'' \prec {t} \land t'' \prec t') \rightarrow ({t} \prec t' \vee {t}=t' \vee t' \prec {t})))\)
(LIN-P) \( FPp \rightarrow Ep\)
(linearity in the past, meaning \(\forall {t}, t', t'' (({t} \prec t'' \land t' \prec t'') \rightarrow ({t} \prec t' \vee {t}=t' \vee t' \prec {t})))\)
(LIN) \((FPp \lor PFp) \rightarrow Ep\)
(linearity)
(DENSE) \(GGp \rightarrow Gp\)  or  \(Fp \rightarrow FFp\)
(density)
(IND\(_{G}\)) \(Fp \wedge G(p \rightarrow Fp )\rightarrow GFp\)
(forward induction)
(IND\(_{H}\)) \(Pp \wedge H(p\rightarrow Pp)\rightarrow HPp\)
(backward induction)
(WELLORD) \(H(Hp \rightarrow p)\rightarrow Hp\)
(transitivity plus well-ordering)
(COMPL) \(A(Hp \rightarrow FHp)\rightarrow (Hp \rightarrow Gp)\)
(Dedekind completeness)

Note that IND\(_{G}\) implies backward discreteness and IND\(_{H}\) implies forward discreteness, but not conversely. Recall that the last two properties above, (WELLORD) and (COMPL), are not definable by first-order sentences. Another example of a temporal formula that does not correspond to first-order sentence (unless linearity is assumed) is \({G} F {p}\rightarrow F {G} {p}.\) On the other hand, some simple first-order definable properties of temporal frames, such as irreflexivity, expressed by \(\forall {t} \neg({t} \prec {t}),\) are not defined by any temporal formula. For more on temporal axioms expressing properties of time and details on such results, see Segerberg (1970); Rescher and Urquhart (1971); Burgess (1979); van Benthem (1983; 1995); and Goldblatt (1987).

3.6.2 Some axiomatic extensions of \(\mathbf{K}_{t}\)

By extending \(\mathbf{K}_{t}\) with suitable additional axioms, one can capture the validities of a number of natural linear models for the flow of time. That is, these axiomatic extensions are sound and complete for the corresponding temporal frames or classes of temporal frames.

\[\begin{align} \mathbf{K4}_{t} &= \mathbf{K}_{t} + \text{(TRAN): all transitive frames.} \\ \mathbf{S4}_{t} &= \mathbf{K}_{t} + \text{(REF) + (TRAN): all partial orderings.} \\ \mathbf{L}_{t} &=\mathbf{K}_{t} + \text{(TRAN) +(LIN): all strict linear orderings.} \\ \mathbf{N}_{t} &=\mathbf{L}_{t} + \text{(NOEND) + (IND\(_{G}\)) + (WELLORD): } \langle \mathbf{N,\lt}\rangle. \\ \mathbf{Z}_{t} &=\mathbf{L}_{t} + \text{(NOBEG) + (NOEND) + (IND\(_{G}\)) + (IND\(_{H}\)): } \langle \mathbf{Z,\lt}\rangle. \\ \mathbf{Q}_{t} &=\mathbf{L}_{t} + \text{(NOBEG) + (NOEND) + (DENSE): } \left\langle \mathbf{Q, \lt}\right\rangle. \\ \mathbf{R}_{t} &=\mathbf{L}_{t} + \text{(NOBEG) + (NOEND) + (DENSE) + (COMPL): } \left\langle \mathbf{R, \lt}\right\rangle. \end{align}\]

All these logics turn out decidable (i.e. have decidable sets of validities) which is typically shown by proving the finite model property, meaning that every satisfiable formula is satisfiable in a finite model; in most cases, with respect to non-standard finite models. For detailed proofs of completeness of variations of these axiomatic systems, as well as proofs of decidability, see Segerberg (1970); Rescher and Urquhart (1971); Burgess (1979); Burgess and Gurevich (1985); and Goldblatt (1987).

Some of these extensions were already being studied in the early days of Tense Logic, and Prior (1967) reported on extensive work on various systems obtained by postulating different combination of axioms. As always, his main focus was on the light thrown by a logical treatment of time 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 temporal formula \(F {p}\rightarrow\Box F {p}.\) See also Thomason (1984) and Finger et al. (2002).

4. Extensions of TL over linear time flows

Though only presented informally, Prior’s original semantics for TL apparently assumed a linear time flow, while being indifferent to other aspects such as discreteness versus density. Here we outline some of the more important extensions of TL with additional temporal operators for linear models of time.

4.1 Adding the “next time” operator

In linear, unbounded, forward-discrete temporal models \(\mathcal{M}= \left\langle T,\prec, V \right\rangle,\) where every instant \(t\) has a (unique) immediate successor \(s(t),\) it is natural to add a new temporal operator \(X,\) neXttime (or, tomorrow), with semantics:

\[ \mathcal{M},t \models X\varphi \text{ iff } \mathcal{M},s(t) \models \varphi. \]

The operator \(X\) satisfies the K-axiom

  • (K\(_{X}\)) \(X(\varphi \to \psi) \to (X\varphi \to X\psi),\)

and, on forward-discrete linear models, the functionality axiom:

  • (FUNC) \(X\lnot \varphi \leftrightarrow \lnot X\varphi.\)

It also enables a recursive definition of \(G:\)

  • (FP\(_G\)) \(G\varphi \leftrightarrow (\varphi \wedge XG\varphi),\) if \(\prec\) is assumed reflexive, or
  • (FP\(^{ir}_G\)) \(G\varphi \leftrightarrow X(\varphi \wedge G\varphi ),\) if \(\prec\) is assumed irreflexive.

On the ordering of natural numbers \( \left\langle \mathbf{N,<}\right\rangle,\) the operators \(X\) and \(G\) also satisfy an induction principle; the reflexive version of this is:

  • (IND) \(\varphi \wedge G(\varphi \rightarrow X\varphi )\rightarrow G\varphi.\)

In fact, in the language with \(G,H\) and \(X\) the following system:

\(\mathbf{L}_{t}(X) = \mathbf{L}_{t}\) + K\(_{X}\) + FUNC + FP\(_{G}\)
axiomatizes completely the temporal logic of unbounded, forward-discrete linear orderings, while

\(\mathbf{N}_{t}(X) = \mathbf{N}_{t}\) + K\(_{X}\) + FUNC + FP\(_{G} \) + IND
axiomatizes completely the temporal logic of \(\left\langle \mathbf{N},s,< \right\rangle,\) where \(s(n) = n+1.\)

The past analogue \(Y\) (Yesterday) of \(X,\) can be defined and axiomatized likewise.

For more detail see Thomason (1984), Goldblatt (1987), and Andréka et al. (1995).

4.2 Adding Since and Until

Prior’s basic Tense Logic with the “PFGH” syntax is not very expressive and since its introduction various extensions have been proposed, already by Prior himself. Perhaps the most important of them is the introduction of the binary temporal operators \(S\) (“Since”) and \(U\) (“Until”) by Hans Kamp in his doctoral dissertation (Kamp 1968). The intuitive meanings of these are[2]

  • \(\varphi S\psi\) “\(\varphi\) has been true since a time when \(\psi\) was true”
  • \(\varphi U\psi\) “\(\varphi\) will be true until a time when \(\psi\) is true”

For instance (noting that ‘unless’ is just another way to express disjunction), the sentence “I will keep trying until I succeed, unless I die meanwhile” can be formalised using Until and the special atomic propositions \(\mathrm{try}, \mathrm{succeed}, \mathrm{die}\) as: \( \mathrm{try}\, U(\mathrm{succeed} \lor \mathrm{die}).\) As another example, “Ever since Mia left home, Joe has been unhappy and has been drinking until losing consciousness, over and over again” can be formalised using Since and Until as:

\[ (\text{Joe unhappy} \land (\text{Joe drinking}\ U\lnot(\text{Joe conscious})))\ S(\text{Mia leaves home}). \]

The formal semantics of \(S\) and \(U\) in temporal models can be given as:

\[\begin{align} \mathcal{M},t\vDash \varphi S\psi \text{ iff } &\mathcal{M},s\vDash \psi \text{ for some } s \text{ such that } s\preceq t \\ & \text{ and } \mathcal{M},u\vDash \varphi \text{ for every } u \text{ such that } s\preceq u\prec t. \\ \mathcal{M},t\vDash \varphi U\psi \text{ iff } &\mathcal{M},s\vDash \psi \text{ for some } s \text{ such that } t\preceq s \\ & \text{ and } \mathcal{M},u\vDash \varphi \text{ for every } u \text{ such that } t\preceq u\prec s. \end{align}\]

These are the semantic definitions of the reflexive versions of \(U\) and \(S,\) as they include the possibility of \(\psi \) holding at the current instant, and then nothing is required about \(\varphi.\) Prior’s basic tense operators (in their reflexive versions) can be expressed using \(U\) and \(S\) as \(F\varphi :=\top U\varphi\) and \(P\varphi :=\top S\varphi,\) while \(X\) cannot be expressed. These are the versions traditionally adopted in computer science. However, one may argue that a more natural definition of \(U\) and \(S\) would be one where the instant \(s\) is required to be strictly in the future (resp., in the past) of \(t\) and that no requirement for the truth of \(\varphi\) is imposed on the current instant. These are the irreflexive, or strict versions, which we denote by \(U^{s}\) and \(S^{s}.\) They are more expressive. In particular, the operator \(X\) and the reflexive \(U\) and \(S\) are definable in terms of \(U^{s}\) and \(S^{s}:\)

\[\begin{align} X\varphi &:= \bot U^{s} \varphi, \\ \varphi U\psi &:=\psi \vee (\varphi \land \varphi U^{s}\psi), \\ \varphi S\psi &:=\psi \vee (\varphi \land \varphi S^{s}\psi), \end{align}\]

but generally not vice versa. Still, on forward discrete linear frames \(U^{s}\) can be defined in terms of \(U\) and \(X:\) \(\varphi U^{s}\psi = X(\varphi U\psi).\) Likewise, \(S^{s}\) can be defined from \(S\) on backward discrete frames using the past analogue of \(X.\)

Various other natural operators can be defined in terms of \(U\) and \(S\) or their strict versions, for instance Before, defined as \(\varphi B\psi :=\lnot ((\lnot \varphi )U\psi)\) and meaning “\(\varphi\) will occur before \(\psi\) (which may or may not occur at all)”.

Hans Kamp (1968) proved the following remarkable expressive completeness result about the temporal language with Since and Until:

Every temporal operator on a class of Dedekind complete linear orderings which is definable in first order logic is expressible in terms of \(S^{s}\) and \(U^{s}\).

J. Stavi later proposed two more operators, \(S^{\prime}\) and \(U^{\prime}\) which when added to \(S^{s}\) and \(U^{s}\) make the temporal language expressively complete on all linear frames, see e.g. (Gabbay et al. 1994). On the other hand, Gabbay has shown (ibid.) that no finite number of new operators can make the temporal language functionally complete on all partial orderings.

Burgess (1982a) provided a complete axiomatic system of the Since–Until logic on the class of all linear time flows, further simplified by Xu (1988). It extends the classical propositional logic with the following axiom schemata (for the reflexive versions) and their duals, with \(S\) and \(U\) swapped:

\(G\varphi \rightarrow \varphi,\)
\(G(\varphi \rightarrow \psi )\rightarrow \varphi U\chi \rightarrow \psi U\chi,\)
\(G(\varphi \rightarrow \psi )\rightarrow \chi U\varphi \rightarrow \chi U\psi,\)
\(\varphi \wedge \chi U\psi \rightarrow \chi U(\psi \wedge \chi S\varphi ),\)
\(\varphi U\psi \rightarrow (\varphi \wedge \varphi U\psi )U\psi,\)
\(\varphi U(\varphi \wedge \varphi U\psi )\rightarrow \varphi U\psi ;\)
\(\varphi U\psi \wedge \chi U\theta \rightarrow (\varphi \wedge \chi )U(\psi \wedge \theta )\vee (\varphi \wedge \chi )U(\psi \wedge \chi )\vee (\varphi \wedge \chi )U(\varphi \wedge \theta ).\)

and the inference rules NEC\(_{H}\) and NEC\(_{G}.\) This axiomatization, translated for the strict versions \(S^{s}\) and \(U^{s},\) was extended by Venema (1993) to complete axiomatic systems for \(S^{s}\) and \(U^{s}\) for:

  • all discrete linear orderings, by adding \(F^{s}\top \rightarrow \bot U^{s}\top\) and its dual \(P^{s}\top \rightarrow \bot S^{s}\top.\)
  • all well-orderings, by further adding \(H^{s}\bot \vee P^{s}H^{s}\bot\) and \(F^{s}\varphi \rightarrow (\lnot \varphi )U^{s}\varphi ,\)
  • \(\left\langle \mathbf{N,<}\right\rangle,\) by adding \(F^{s}\top\) to the previous system.

For further details and other related results see Burgess (1984), Thomason (1984), Gabbay et al. (1994), Finger et al. (2002), Hodkinson and Reynolds (2006).

4.3 The linear time temporal logic LTL

The most popular and widely used temporal logic in computer science is the linear time temporal logic LTL, proposed in the seminal paper Pnueli (1977) and first explicitly axiomatized and studied in Gabbay et al. (1980). LTL involves \(X,\) \(G\) and \(U\) only (no past operators), interpreted on \(\left\langle \mathbf{N,<}\right\rangle,\) and is very useful for expressing safety, liveness, fairness, and precedence properties of infinite computations in reactive systems Manna and Pnueli (1992); see explanation of these properties in 10.1 Section. An example of such specification: “Every time when a message is sent, an acknowlegment of receipt will eventually be returned and the message will not be marked ‘sent’ before an acknowledgment of receipt is returned”, formalisable in LTL as:

\[ G(\mathrm{Sent} \to (\lnot \mathrm{MarkedSent} \ U\ \mathrm{AckReturned})). \]

Here is a complete axiomatic system for LTL, extending the classical propositional logic only with the standard K axioms for \(G\) and \(X\) and inference rules MP and NEC\(_{G},\) plus axioms expressing fixed-point characterisations of \(G\) and \(U:\)

  • (K\(_G\)) \(G(\varphi \rightarrow \psi )\rightarrow (G\varphi \rightarrow G\psi)\)
  • (K\(_X\)) \(X(\varphi \rightarrow \psi )\rightarrow (X\varphi \rightarrow X\psi )\)
  • (FUNC) \(X\lnot \varphi \leftrightarrow \lnot X\varphi\)
  • (FP\(_G\)) \(G\varphi \leftrightarrow (\varphi \wedge XG\varphi )\)
  • (GFP\(_G\)) \(\psi \land G(\psi \rightarrow (\varphi \land X\psi)) \rightarrow G\varphi\)
  • (FP\(_U\)) \(\varphi U\psi \leftrightarrow (\psi \vee (\varphi \wedge X(\varphi U\psi )))\)
  • (LFP\(_U\)) \(G((\psi \vee (\varphi \wedge X\theta))\rightarrow \theta )\rightarrow (\varphi U\psi \rightarrow \theta )\)

In technical terms, the axiom FP\(_{G}\) says that \(G\varphi\) is a fixed point of the operator \(\Gamma_{G}\) defined by \(\Gamma_{G} (\theta) = \varphi \land X\theta,\) whereas GFP\(_{G}\) says that \(G\varphi\) is (set-theoretically, in terms of its extensions) a greatest post-fixed point of \(\Gamma_{G} .\) Likewise, the axiom FP\(_{U}\) says that \(\varphi U\psi\) is a fixed point of the operator \(\Gamma_{U}\) defined by \(\Gamma_{U}(\theta) = \psi \lor (\varphi \land X\theta),\) whereas LFP\(_{U}\) says that \(\varphi U\psi\) is a least pre-fixed point of \(\Gamma_{U}.\) Note that GFP\(_{G}\) generalises the Induction axiom (IND): \(\varphi \wedge G(\varphi \rightarrow X\varphi)\rightarrow G\varphi.\) In fact, the axiom GFP\(_{G}\) can be replaced by the following Induction rule, derivable in the system above:

If \(\vdash \psi \rightarrow \varphi \land X\psi\) then \(\vdash \psi \rightarrow G\varphi.\)

Likewise, LFP\(_{U}\) can be replaced by the following derivable rule:

If \(\vdash (\psi \vee (\varphi \wedge X\theta)) \rightarrow \theta\) then \(\vdash \varphi U\psi \rightarrow \theta.\)

Actually, after defining \(Gp\) as \(\lnot (\top U\lnot p),\) the axioms FP\(_{G}\) and GFP\(_{G}\) become derivable from the rest.

Proofs of completeness of variations of the axiomatic system above can be found in Gabbay et al. (1980; 1994) and Goldblatt (1987).

All logics mentioned in this section have the finite model property (usually, with respect to non-standard models) and therefore are decidable. Proofs of decidability can be found in the references on completeness.

5. Branching time temporal logics

As noted earlier, the idea of time flows with deterministic, linear past and non-deterministic, branching future has a venerable history; we have already mentioned the different views associated with Ockham and Peirce (Section 1). The idea of time with branching future has also been entertained in the non-scientific literature, for example J. Borges’ “The garden of forking paths”, as well as in numerous science fiction writings.

5.1 Prior’s branching time logics of historical necessity

Prior argued that the fallacy of Diodorus’ Master Argument lay in his assumption that whatever is, or is not, or will be, or will never be, has in the past been necessarily so – thus, in effect assuming that the future is deterministic. In his analysis, Prior supported Aristotle’s view that “while it is now beyond the power of men or gods to affect the past, there are alternative futures between which choice is possible”. In order to resolve the problems pointed out by Aristotle and Diodorus, Prior wanted, inter alia, to capture the logic of historical necessity. His philosophical analysis and the quest for formalisation of the arguments for “the incompatibility of foreknowledge (and fore-truth) and indeterminism” lead him to consider two formalizations of temporal logic of branching time, reflecting the “Ockhamist” (or “actualist”) and “Peircean” views mentioned earlier. For details on Prior’s views and motivating analyses, see Prior (1967, Ch. VII), Rescher and Urquhart (1971, Ch. VII), Øhrstrøm and Hasle (1995, Chs. 2.6 and 3.2) and the entry on Arthur Prior.

5.2 The Ockhamist temporal logic

The Ockhamist semantics for temporal logic was intuitively conceived by Prior but formally developed later, in Burgess (1979); see also Øhrstrøm and Hasle (1995) and Thomason (1984). It is based on the assumption that while the past cannot be changed, the future can take different possible courses from the present moment; however, at every moment one possible future is considered actual, and it is in relation to this future that future-tense statements are evaluated. Thus, the phrases ‘always / sometime in the future’ now mean ‘always / sometime in the future considered actual’. Furthermore, that actual future is considered determined, i.e., linear. Formally, this means, first, that the natural flows of time for Ockhamist semantics are tree-like rather than linear, and second, that temporal formulae are evaluated relative not only to a time instant, but also to a history containing that instant. We note, however, that according to Belnap (2001, Ch. 6) the notion of “actual future” is problematic and he would simply say that tensed formulae are in general neither true nor false at a moment; they are true or false at pairs (moment, history), but without any commitment to the existence of an “actual future”. Moreover, Belnap and Green (1994) argue that such “actual future”, which they call “the Thin Red Line”, is not a sustainable idea and “one can make sense of an indeterministic, branching structure for our world without postulating an actual future as distinguished among the possibilities”, instead promoting the idea of “open future”.

In either case, in order to refer to, and quantify over, the possible histories passing through the current instant, an additional modal operator \(\diamondsuit\) and its dual \(\Box\) are introduced, with \(\diamondsuit \varphi\) declared true at (\({h},{t}\)) if there is some history \(h'\) through \(t\) such that \(\varphi\) is true at (\({h'},{t}\)). Then \(\diamondsuit F \varphi\) says that “\(\varphi\) holds eventually in some possible future”, while \(\Box F \varphi\) says that “\(\varphi\) holds eventually in all possible futures”, i.e., will necessarily, inevitably eventually be the case.

Formally, the language of propositional Ockhamist branching-time temporal logic, OBTL, contains, besides the temporal modalities \(F,P,\) a modality \(\diamondsuit\) for referring to the possible histories passing through the current instant. The formulae of OBTL are defined accordingly:

\[\varphi =\bot \mid p\mid \varphi \rightarrow \varphi \mid P\varphi \mid F\varphi \mid \diamondsuit \varphi.\]

For instance, the sentence “Life on Earth will eventually cease to exist” refers only to the currently regarded as actual future and translates in OBTL simply as \( F\lnot \text{LifeOnEarth},\) while “Life on Earth will eventually cease to exist if a new war breaks out, but the humanity can change the course of history to avoid a new war” would naturally translate in OBTL as

\[ (F\text{ War} \to F\lnot \text{LifeOnEarth}) \land \Diamond \lnot F\text{ War}. \]

For a more involved example: “On every possible future where life on Earth will eventually cease to exist, every day when there is life on Earth the humanity can possibly change the course of history so that there will be life on Earth the day after” can be translated as

\[ \Box( F\lnot \text{LifeOnEarth} \to G(\text{LifeOnEarth} \to \Diamond X\, \text{LifeOnEarth})). \]

To formally describe Ockhamist semantics we need some technical definitions. (They differ slightly from those of Burgess (1979) but are equivalent to them.) A temporal frame \(\mathcal{T}= \left\langle T, \prec \right\rangle\) is a tree if \(\prec\) is a partial ordering on \(T\) and every instant \(t\in \mathcal{T}\) has a linearly ordered set of \(\prec\)-predecessors in \(\mathcal{T}.\) A history in a tree is a maximal (i.e., not extendable) set of instants linearly ordered by \(\prec.\) We denote the set of all histories in \(\mathcal{T}\) by \(\mathcal{H}(\mathcal{T}).\) The branch on a history \(h\) starting at an instant \(t\in h\) is a pair \((h,t)\) consisting of the part of \(h\) above \(t,\) i.e., the set of all instants \(t'\) on \(h\) such that \(t\preceq t'.\) The set of histories passing through an instant \(t\) in \(\mathcal{T}\) will be denoted by \(\mathcal{H}(t).\) Intuitively, a branch \((h,t)\) represents an instant \(t\) together with its actual future.

A valuation in a tree \(\left\langle T, \prec \right\rangle\) is a mapping \(V\) which assigns to every atomic proposition \(p \in {PROP}\) a set of branches \(V(p) \subseteq \mathcal{H}\times T\) on which \(p\) is declared true. Thus, the Ockhamist truth of an atomic proposition depends both on the time instant and on the possible future on which it is considered. An Ockhamist tree model is a tuple \(\mathcal{M}= \left\langle T, \prec, V \right\rangle\) where \(\left\langle T, \prec \right\rangle\) is a tree and \(V\) is a valuation in it. Now, the definition of (Ockhamist) truth of a formula of OBTL in \(\mathcal{M},\) relative to a branch \((h,t)\) where \(h \in \mathcal{H}\) and \(t\in h\), is given recursively as follows:

\[\begin{align} \mathcal{M},h,t &\models p \text{ iff } (h,t)\in V(p), \text{ for any } p\in {PROP}, \\ \mathcal{M},h,t &\not\models\bot, \\ \mathcal{M},h,t &\models \phi \lor \psi \text{ iff } \mathcal{M},h,t\models \phi \text{ or } \mathcal{M},h,t\models \psi,\\ \mathcal{M},h,t &\models F\phi \text{ iff } \mathcal{M},h,t'\models \phi \text{ for some } t'\in h \text{ such that } t \prec t'. \\ \mathcal{M},h,t &\models P\phi \text{ iff } \mathcal{M},h,t'\models \phi \text{ for some } t'\in h \text{ such that } t' \prec t. \\ \mathcal{M},h,t &\models \diamondsuit \phi \text{ iff } \mathcal{M},h',t\models \phi \text{ for some } h'\in \mathcal{H}(t). \end{align}\]

We now say that a formula of OBTL is Ockhamist valid if it is true on every branch of every Ockhamist tree model.

Prior (1967) held that atoms should “contain no trace of futurity” and their truth should only depend on the current time instant, but not on the current history. So, he considered two versions of the Ockhamist logic: one, only involving such ‘no futurity’ atoms, which we will call ‘instant-based atomic propositions’, and the other involving both sorts of atomic propositions. Actually, instant-based atoms can be simulated by ‘(instant,history)’-type atomic propositions by prefixing with \(\Box,\) since the truth of \(\Box p\) does not depend on the current history but only on the current time point.

In general, not all histories in the temporal frame may be of interest, and in order to define Ockhamist type semantics it suffices to consider rich enough families of histories, called a bundles. A bundled tree is a pair \((\mathcal{T}, \mathcal{B})\) where \(\mathcal{T}\) is a temporal frame \(\mathcal{T}= \left\langle T, \prec \right\rangle\) which is a tree and \(\mathcal{B}\) is a non-empty set of histories in \(\mathcal{T}\) (the bundle), such that every instant of \(\mathcal{T}\) belongs to some history from \(\mathcal{B}.\) A valuation in a bundled tree \((\mathcal{T}, \mathcal{B})\) is a mapping \(V\) which assigns to every \(p \in {PROP}\) a set of branches \(V(p) \subseteq \mathcal{B}\times T.\) A bundled tree model is a bundled tree endowed with a valuation. A complete bundled tree is a bundled tree of the type \((\mathcal{T},\mathcal{H}(\mathcal{T})),\) i.e., where the bundle consists of all histories in the tree. Now, the semantics for OBTL is readily generalised to bundled tree models, simply by relativising all clauses of the truth definition to the histories in \(\mathcal{B}.\) In particular, now \(\diamondsuit\) only refers to those histories. We say that a formula of OBTL is bundled tree valid (BT-valid) if it is true on every branch of every bundled tree model. We note that, as proved in Zanardo et al. (1999), the class of complete bundled trees is not definable by Ockhamist formulae within the class of all bundled trees, so results about definability and completeness do not readily transfer in either direction.

Abstract analogues of bundled trees, called \(T\times W\)-frames or Kamp frames by Thomason (1984) and technically equivalent to Ockhamist frames by Zanardo (1996), can be alternatively used to introduce Ockhamist semantics. In such frames, branches are abstract primitive entities and the relations between branches that correspond to the modal and temporal operators in OBTL are explicitly given as part of the definition of the model. Thus, time is represented as a bundle of histories passing through simultaneous ‘moments’ (in Belnap’s terminology, see Belnap et al. 2001) and instants here are no longer primitive entities, but maximal sets of simultaneous moments. Visually, these are horizontal slices through the bundle of all histories.

On the other hand, it turns out that bundled tree validity is strictly weaker than the Ockhamist validity, i.e., validity restricted to complete bundled trees. Indeed, the following formula is Ockhamist valid: \[\Box G(\Box p \to \diamondsuit F\Box p) \to \diamondsuit G(\Box p \to F\Box p)\] However, as shown in Reynolds (2002), it is not valid in all bundled trees. (Note that, following Prior, Reynolds assumes only instant-based atomic propositions, so the formula above is obtained from Reynolds’ formula by prefixing every occurrence of \(p\) by \(\Box.\)) The reason, intuitively, is that the antecedent allows step-by-step construction of a “limit history”, on which \(\Box q\) holds infinitely often, from an infinite sequence of possibly different histories. All these intermediate histories may belong to the bundle, while the limit history may not be in it. Thus, to completely axiomatize Ockhamist validity we must add axioms that capture the limit closure property of complete bundled trees. Reynolds (2003) proposed complete axiomatic systems for OBTL for both BT-validity and Ockhamist validity, assuming instant-based atomic propositions. The former system extends the axioms for \(G\) and \(H\) on linearly ordered time flows with the S5 axioms for \(\Box,\) the axiom \(G\bot \to \Box G\bot\) implying maximality of histories, the axiom schema

  • (HN) \(P\varphi \to \Box P\diamondsuit \varphi\)

saying that all histories through the current instant share the same past, and the following non-standard (“Gabbay-style”) rule of inference, used to force irreflexivity of the time precedence relation:

\[ \tag{\(\textbf{IRR}\)} \frac{(p\land H\lnot p) \to \varphi}{\varphi}, \text{ assuming that } p \text{ does not occur in } \varphi. \]

In order to completely axiomatize Ockhamist validity, Reynolds adds the following infinite scheme of “limit closure axioms”:

\[\tag{\(\textbf{LC}\)} \Box G_{\leq} \bigwedge_{i=0}^{n-1} (\diamondsuit \varphi_{i} \to \diamondsuit F\diamondsuit \varphi_{i+1}) \to \diamondsuit G_{\leq} \bigwedge_{i=0}^{n-1} (\diamondsuit \varphi_{i} \to F\diamondsuit \varphi_{i+1}) \]

where \(\varphi_{0},\ldots, \varphi_{n-1}\) are any OBTL formulae, \(\varphi_{n} = \varphi_{0},\) and \(G_{\leq} \theta := \theta \land G\theta.\)

Several extensions and variations of OBTL have been proposed and studied. For instance, Brown and Goranko (1999) extend the language of OBTL with a modality for an alternative branch and a special sort of fan-variables representing all histories stemming from one instant, and axiomatise the resulting logic. Another extension along similar lines is Ciuni and Zanardo (2010). For more related results, see also Thomason (1984), Zanardo (1985; 1996), Reynolds (2002; 2003).

5.3 The Peircean temporal logic

In the interpretation of the branching time models of non-deterministic future, called “Peircean” by Prior and apparently favoured by him, \(Fp\) and \(Gp\) are equivalent to the Ockhamist \(\Box Fp\) and \(\Box Gp,\) respectively. Under this interpretation there is no formula equivalent to the Ockhamist \(Fp,\) which is regarded as undetermined. Thus, Peircean temporal logic can be regarded as a proper fragment of Ockhamist temporal logic, obtained by considering only formulae built recursively from atoms using propositional connectives and the combined modalities \(\diamondsuit G,\) \(\diamondsuit F\) and their duals \(\Box G\) and \(\Box F.\) Peircean Branching Time Logic, PBTL, is essentially less expressive than OBTL, lacking equivalents of e.g., \(\diamondsuit GFp\) and \(\diamondsuit FGp\) (for a proof see Reynolds 2002).

Complete finitary axiomatisation of Peircean temporal logic for BT-validity has been obtained by Burgess (1980) using a version of the Irreflexivity rule IRR, and Zanardo (1990) without using such a rule, but with infinitely many axioms, including a very complex axiom schema. See Reynolds (2002) for more details.

5.4 The computation tree logics CTL and CTL*

Branching time logics are much used in computer science. They are variations of the Peircean and Ockhamist logics presented above, but essentially restricted to the class of trees where every history has the order type of the natural numbers. Such trees, called computation trees, are naturally obtained as tree unfoldings of discrete transition systems, hence they naturally represent the tree of all infinite computations arising in such systems. The most popular branching time logics used in computer science are:

  • the computation tree logic CTL, introduced by Clarke and Emerson (1982). This is essentially the Peircean temporal logic interpreted on the class of computation trees without past operators, but only \(G,\) \(X\) (“nexttime”) and \(U\) (“until”). As in the general Peircean temporal logic PBTL, in CTL the temporal operators are always immediately preceded by \(\diamondsuit\) or \(\Box,\) here usually denoted as the quantifiers \(\exists\) and \(\forall\) over histories. CTL was preceded by the logic UB, introduced by Ben-Ari, Manna and Pnueli (1983), in which \(U\) was not used.
  • the full computation tree logic CTL*, introduced by Emerson and Halpern (1985). This is the Ockhamist extension of CTL, with no syntactic restrictions on the applications of temporal operators and path quantifiers, and interpreted on the class of computation trees.

The logic CTL became widely used owing to its good computational properties with regard to model checking, which has linear complexity both in the size of the input formula and in the size of the input model (as a finite transition system). However, it is not very expressive, which led to its extension to CTL*, which is much more expressive and also subsumes the linear time logic LTL, but has higher complexities of model checking (PSPACE) and of satisfiability (2EXPTIME) than CTL. For references and further details, see Emerson (1990) and Stirling (1992).

A complete axiomatisation of CTL can be obtained by replacing the axioms of LTL with their path-quantified versions. For instance, the axioms characterising the temporal operators \(G\) and \(U\) as fixed points now become:

  • (FP\(_{\exists G}\)) \(\exists G\varphi \leftrightarrow (\varphi \wedge \exists X\exists G\varphi);\)
  • (FP\(_{\forall G}\)) \(\forall G\varphi \leftrightarrow (\varphi \wedge \forall X\forall G\varphi );\)
  • (FP\(_{\exists U}\)) \(\exists(\varphi U\psi) \leftrightarrow (\psi \vee (\varphi \wedge \exists X\exists(\varphi U\psi )));\)
  • (FP\(_{\forall U}\)) \(\forall (\varphi U\psi) \leftrightarrow (\psi \vee (\varphi \wedge \forall X\forall (\varphi U\psi ))).\)

For completeness proofs of versions of this axiomatic system for CTL, see Goldblatt (1987) and Emerson (1990).

For CTL* more axioms must be added, to account for the combinations of temporal operators and to enforce the limit closure property. Here are two such additional axioms, the latter being the “limit closure axiom” due to Reynolds (2003):

\(\Box G(\Box \varphi \to \diamondsuit XF\Box \varphi )\to (\Box \varphi \to \diamondsuit GF\Box \varphi );\)
\(\Box G(\diamondsuit \varphi \to \diamondsuit X((\diamondsuit \psi U\diamondsuit \theta)))\to (\diamondsuit \varphi \to \diamondsuit G((\diamondsuit \psi U\diamondsuit \theta))).\)

Obtaining a complete axiomatization for CTL* has turned out much more difficult and the only one known so far, due to Reynolds (2001), involves a very complicated inference rule, extracted from the use of Rabin automata in the proof of completeness. Interestingly, that rule has turned out to be redundant in the extension of CTL* with past operators Reynolds (2005), but it is not known whether it is really needed for derivations in CTL* itself.

We note that all logics mentioned in this section have the finite model property and are decidable. Proofs of decidability of the respective logics can be found e.g. in Burgess (1980), Emerson and Jutla (1984), Gurevich and Shelah (1985), Emerson and Halpern (1985), Goldblatt (1987), Emerson (1990), Gabbay et al. (1994), Finger et al. (2002).

6. Interval temporal logics

While the technical reductions between instant-based and interval based models can be used to reconcile different philosophical and ontological standpoints, they do not resolve the main semantic issue arising when developing logical formalisms for capturing temporal reasoning, viz.: should propositions about time, and therefore formulae in the given logical language, be interpreted as referring to instants or to intervals? The possible natural answers to this question lead to three reasonable alternatives, respectively giving rise to point-based logics discussed above, interval-based logics, and mixed, two-sorted logics, where points and intervals are considered as separate sorts on a par and formulae for both sorts are constructed. We will only discuss here purely interval-based temporal logics, while for a recent study and technical exploration of the two-sorted approach we refer to Balbiani et al. (2011).

There have been various proposals and developments of interval-based temporal logics. Important early philosophical logic papers include Hamblin (1971), Humberstone (1979), Röper (1980), and Burgess (1982b), the latter providing an axiomatization for an interval-based (called there “period-based”) temporal logic involving the earlier/later relation between intervals on the time flows of the rationals and the reals.

The interval-based approach to temporal reasoning has been more prominent in Artificial Intelligence, where some notable works include Allen’s logic of planning (1984), Kowalski and Sergot’s calculus of events (1986), and Halpern and Shoham’s modal interval logic (1986), but also features in some applications to computer science such as real-time logics and hardware verification, notably Moszkowski’s Interval Logic (1983) and Zhou, Hoare and Ravn’s Duration Calculus, see Hansen and Zhou (1997).

Here we will present briefly Halpern and Shoham’s propositional modal interval logic, hereafter called \(\mathsf{HS}.\) It employs a set of unary modal operators corresponding to each of Allen interval relations and having Kripke semantics over that relation. Halpern & Shoham (1986) chose a different notation for Allen relations from the one used by Allen. We compared the two notations in Table 1.

The language of \(\mathsf{HS}\) includes a set of propositional letters \(\mathcal{AP},\) the classical propositional connectives \(\lnot\) and \(\lor\) (all others, including the propositional constants \(\top\) and \(\bot,\) are assumed definable as usual), and a family of interval temporal modal operators (modalities) of the form \(\langle X\rangle,\) one for each of the Allen relations. Formulae are defined by the following grammar: \[\varphi ::= p \mid \neg \varphi \mid \varphi \vee \varphi \mid \langle X \rangle\varphi\]

Given a strict partial ordering \(\mathbb D = \langle D,<\rangle,\) an interval in \(\mathbb D\) is an ordered pair \([d_{0},d_{1}]\) such that \(d_{0},d_{1}\in D\) and \(d_{0}\leq d_{1}.\) The set of all intervals in \(\mathbb{D}\) will be denoted by \(\mathbb{I}(\mathbb{D)}.\) An interval model is a pair \(M\mathbf{=}\left\langle \mathbb{D},V\right\rangle,\) where \(V:\mathbb{I}(\mathbb{D})\rightarrow 2^\mathcal{AP}\) is a labeling assigning to each interval a set of atomic propositions considered true at it. Note that the interval models defined here include “point intervals”, with coinciding endpoints, following the original semantics of \(\mathsf{HS}\) in Halpern & Shoham (1986). Sometimes, “strict” semantics is considered, where point intervals are excluded.

The truth of a formula over a given interval \([a,b]\) in an interval model \(M\) is defined by usual structural induction on formulae:

\[\begin{array}{ll} M,[a,b] \models p &\text{ iff } p \in V([a,b]), \text{ where } p \in \mathcal{AP}; \\ M,[a,b] \models \neg\psi &\text{ iff } M,[a,b]\not\models\psi; \\ M,[a,b] \models \varphi \vee \psi &\text{ iff } M,[a,b]\models\varphi \text{ or } M,[a,b]\models\psi; \\ M,[a,b] \models \langle Z\rangle\psi &\text{ iff } \text{there is an interval } [c,d] \text{ such that } [a,b]R_{Z}[c,d] \\ & \quad \text{and } M,[c,d]\models\psi, \text{ where } R_Z \text{ is } \langle Z\rangle \text{ (Table 1)}. \end{array}\]

E.g., \(M,[d_{0},d_{1}] \models \langle A \rangle\varphi\) iff \(M,[d_{1},d_{2}] \models \varphi\) for some interval \([d_{1},d_{2}].\)

For each diamond modality \(\langle Z\rangle,\) the corresponding box modality is defined as a dual: \([Z] \varphi \equiv \neg \langle Z\rangle \neg \varphi.\)

Sometimes it is useful to consider an additional modal constant for point intervals, denoted \(\pi,\) with the following truth definition:

\[ M,[d_{0},d_{1}]\models\pi \text{ iff } d_{0}=d_{1}. \]

Some of the \(\mathsf{HS}\) modalities are definable in terms of others and for each of the strict and non-strict semantics, minimal fragments that are expressive enough to define all other operators have been identified:

  • In the strict semantics, the six modalities \(\langle A \rangle,\) \(\langle B \rangle,\) \(\langle E \rangle,\) \(\langle \overline{A} \rangle,\) \(\langle \overline{B} \rangle,\) \(\langle \overline{E} \rangle\) suffice to express all others, as shown by the following equivalences:

    \[\begin{matrix} \langle L\rangle\varphi \equiv \langle A \rangle\langle A \rangle\varphi, & \langle \overline{L}\rangle\varphi \equiv \langle\overline{A}\rangle\langle\overline{A}\rangle\varphi, \\ \langle D\rangle\varphi \equiv \langle B\rangle\langle E\rangle\varphi, & \langle\overline{D}\rangle\varphi \equiv \langle\overline{B}\rangle\langle\overline{E}\rangle\varphi, \\ \langle O\rangle\varphi \equiv \langle E\rangle\langle\overline{B}\rangle\varphi, & \langle\overline{O}\rangle\varphi \equiv \langle B\rangle\langle\overline{E}\rangle\varphi. \end{matrix}\]

  • In the non-strict semantics, the four modalities \(\langle B \rangle,\) \(\langle E \rangle,\) \(\langle \overline{B} \rangle,\) \(\langle \overline{E} \rangle\) suffice to express all others, as shown by the following equivalences:

    \[\begin{align} \langle A \rangle\varphi &\equiv ([E]\bot \wedge (\varphi \vee \langle\overline{B}\rangle\varphi)) \vee \langle E\rangle([E]\bot \wedge (\varphi \vee \langle\overline{B}\rangle\varphi)), \\ \langle\overline{A}\rangle\varphi &\equiv ([B]\bot \wedge (\varphi \vee \langle\overline{E}\rangle\varphi)) \vee \langle B\rangle([B]\bot \wedge (\varphi \vee \langle\overline{E}\rangle\varphi)), \\ \langle L\rangle\varphi &\equiv \langle A \rangle(\langle E\rangle\top \wedge \langle A \rangle\varphi), \\ \langle \overline{L}\rangle\varphi &\equiv \langle\overline{A}\rangle(\langle B\rangle\top \wedge \langle\overline{A}\rangle\varphi), \\ \langle D\rangle\varphi &\equiv \langle B\rangle\langle E\rangle\varphi, \\ \langle\overline{D}\rangle\varphi &\equiv \langle\overline{B}\rangle\langle\overline{E}\rangle\varphi, \\ \langle O\rangle\varphi &\equiv \langle E\rangle(\langle E\rangle\top \wedge \langle\overline{B}\rangle\varphi), \\ \langle\overline{O}\rangle\varphi &\equiv \langle B\rangle(\langle B\rangle\top \wedge \langle\overline{E}\rangle\varphi). \end{align}\]

    Also, the modal constant \(\pi\) is definable in terms of \(\langle B \rangle\) and \(\langle E \rangle,\) respectively as \([B]\bot\) and \([E]\bot.\)

The logic \(\mathsf{HS}\) has over a thousand expressively non-equivalent fragments involving only some of the modal operators, which have been studied extensively (see (Della Monica et al, 2011) for a survey). \(\mathsf{HS}\) and most of its fragments are very expressive and the validity in them is usually undecidable (under some additional assumptions, even highly undecidable, viz. \(\Pi^{1}_{1}\)-complete). However, some quite non-trivial decidable cases of fragments of HS have been identified. Probably the best studied expressive interval logics are the neighborhood interval logics (Goranko et al, 2003), involving the modal operators \(\langle A \rangle\) and \(\langle\overline{A}\rangle.\) One specific axiom for \(\langle A \rangle\) (and, symmetrically for \(\langle\overline{A}\rangle\)) is \(\langle A \rangle\langle A \rangle\langle A \rangle p \to \langle A \rangle\langle A \rangle p,\) saying that any two consecutive right-neighboring intervals can be joined into one right-neighboring interval.

There is a natural spatial interpretation of interval temporal logics, based on the idea that every interval on a linear ordering \(L\) is represented as a pair of points (beginning,end), which can be treated as coordinates of a point in the \(L \times L\)-plane, and relations between intervals have natural corresponding spatial relations between their representing points. This interpretation has been fruitfully explored to relate various technical results, such as undecidability, between spatial and interval logics, see e.g., Venema (1990), Marx and Reynolds (1999). For details and more on interval temporal logics see Halpern & Shoham (1986), Venema (1990), Goranko et al. (2003), Goranko et al. (2004), Della Monica et al. (2011), the survey Konur (2013), and the references therein.

Besides the unary interval modalities associated with the binary Allen interval relations, there is a natural and important operation of chopping an interval into two subintervals, which gives rise to the ternary interval relation ‘chop’, proposed and studied in Moszkowski (1983) and later extended in Venema (1991) to the logic CDT, involving ‘chop’ (\(C\)) and the two residual ‘chop’ operators \(D\) and \(T.\) The logic CDT was completely axiomatised in Venema (1991), see also Goranko et al. (2004) and Konur (2013).

Lastly, a few words about the relationships between the expressiveness of the languages of interval temporal logics and first-order logic. The standard translation ST of Prior’s Tense Logic to first-order logic, presented in Section 3.3, extends naturally to interval logics, where atomic propositions are represented in the first-order language by binary relations. It turns out that there is a natural match between interval temporal logics and bounded-variable fragments of first-order logic: some of the \(\mathsf{HS}\) modalities can be translated into the two-variable fragment FO\(^{2}\) of first-order logic, which eventually implies their decidability, while the rest require at least 3 distinct variables for the standard translation. It was shown in Bresolin et al. (2009) that the expressively strongest such interval logic is the neighborhood interval logic, which was proved there to be expressively complete for FO\(^{2}.\) On the other hand, even the full \(\mathsf{HS}\) is less expressive than the three-variable fragment FO\(^{3},\) for which Venema (1991) proved that the logic CDT is expressively complete.

7. Other variants of temporal logics

So far we have discussed the traditional hierarchy of temporal logics, but there are numerous alternative developments which do not fit this hierarchy, and yet can be useful formalisms for various applications. We briefly present some of them here.

7.1 Hybrid temporal logics

A notable development, enriching the traditional framework of temporal logics, is to incorporate features of first-order logic to produce a family of so-called hybrid logics, that blend together the language and metalanguage of temporal logic. Hybrid logics are very expressive, yet they often preserve the good computational properties of standard temporal logic. They include several syntactic mechanisms which extend the classical temporal framework, some of which go back to Prior’s work (see Blackburn 2006) and these are briefly mentioned below, approximately in order of increasing expressiveness. See more details and references e.g., in Goranko (1996), Areces and ten Cate (2006) and the entry on hybrid logics.

  • Universal modality \(A\) (meaning in temporal terms “always”), interpreted by the universal relation of the temporal frame. Using \(A\) one can express global statements locally, such as validity in a model \(\mathcal{M}\): \(\mathcal{M},t\vDash A\varphi\) iff \(\mathcal{M}\vDash A\varphi.\)
  • Nominals, aka clock variables. These are special atomic propositions which are bound to be true at exactly one instant of the model, i.e., one can think of a clock variable \(t\) saying “It is \(t\) o’clock now”. The idea of nominals goes back to Prior (1967), but has been independently developed and applied in several more recent works, see references above.
  • Satisfaction operator \(@_{i},\) where \(i\) is a nominal, with semantics \(M,t\vDash @_{i}\varphi\) iff \(M,V(i)\vDash \varphi,\) where \( V(i)\) is the unique instant where \(i\) is true. Thus, the basic semantic notion of a truth at an instant of a model is now brought into the syntax. Besides increasing the expressiveness, this also allows for an elegant development of proof systems such as sequent calculi and semantic tableaux in the style of labelled deduction.
  • Difference modality \(D\varphi,\) saying that \(\varphi \) is true at some other instant. The expressiveness of the resulting language is in a sense equivalent to the one with nominals and universal modality.
  • Reference pointers, aka binders: \(\downarrow_{i},\) where \(i\) is a nominal. These behave syntactically as quantifiers, and the semantic effect is that \(\downarrow _{i}\) binds the value of the nominal \(i\) to the current instant of evaluation. Formally, \(\mathcal{M},t\vDash \downarrow_{i}\varphi\) iff \(\mathcal{M}_{[i\rightarrow t]},t\vDash \varphi,\) where \(\mathcal{M}_{[i\rightarrow t]}\) is the model obtained from \(\mathcal{M}\) by re-assigning the denotation of \(i\) to be \(t.\) The introduction of reference pointers in Goranko (1996) was partly motivated by the idea of adding a syntactic mechanism for referring to the current time instant, i.e. saying ‘Now’. For a systematic logical analysis and formal treatment of Now see Kamp (1971). A similar referencing mechanism, called freeze quantifier, binding a variable to the time of the local temporal context, was introduced in Alur and Henzinger (1994).
  • Quantifiers over nominals: \(\forall i\varphi,\) where \(i\) is a nominal. The semantics should be clear: \(M,t\vDash \forall i\varphi\) iff \(M_{[i\rightarrow s]},t\vDash \varphi\) for any instant \(s\in M.\) These bring the full power of first-order quantification to the temporal language, while still preserving many of its propositional virtues. The idea goes back to Bull (1970).
  • Propositional quantifiers: \(\forall p\varphi\) where \(p\) is an atomic proposition. This is a second-order quantification brought into the propositional language and leads to a leap in expressiveness often resulting in recursive non-axiomatizability. We briefly discuss propositional quantification in temporal logics further.

Hybrid languages are quite expressive. Here are just two examples:

  • defining irreflexivity of the precedence relation, which is not expressible in TL, even if extended with the reflexive \(U,\) is straightforward in a language with nominals and \(@\) as \(@_{i}G\lnot i.\)
  • The operators \(S\) and \(U\) (in any variation) are definable in the hybrid language with nominals and binders: \(\varphi U\psi :={\downarrow _{i}}F(\psi \wedge H(Pi\rightarrow \varphi ))\) and likewise for \(S.\)

While the weaker versions of hybrid logics – with universal modality and nominals or with difference modality – are still decidable, the more expressive ones, involving reference pointers / binders or quantifiers over nominals are usually undecidable, see Goranko (1996), Areces and ten Cate (2006).

7.2 Metric and real-time temporal logics

Metric temporal logics go back to Prior, too. He used the notation \(Fnp\) to mean “It will be the case the interval \(n\) hence that \(p\)” (that is, \(p\) will be the case after \(n\) time units) and \(Pnp\) for “It was the case the interval \(n\) ago that \(p\)” (that is, \(p\) was the case before \(n\) time units). The latter he regarded as an abbreviation of \(F(-n)p.\) The case \(n=0\) gives us the present tense. We can define the general, non-metric operators respectively by

\[\begin{matrix} Pp \equiv \exists {n}({n} \lt 0 \land Pnp), & Fp \equiv \exists n(n \gt 0 \land Fnp); \\ Hp \equiv \forall {n}({n} \lt 0 \rightarrow Pnp), & Gp \equiv \forall n(n \gt 0 \rightarrow Fnp). \end{matrix}\]

Systems of instant-based temporal logics for metric time and ‘Chronological logic’ were introduced and studied in (Rescher and Urquhart, 1971, Chapter X). For more on metric (and layered) temporal logics see Montanari (1996) and Montanari and Policriti (1996). For metric neighborhood interval logics see Bresolin et al. (2013).

Various real-time extensions of temporal logics have also been proposed and studied, for instance by adding:

  • time-bounded operators, e.g.: \(G(p \to F_{_{\leq 3}} q).\)
  • freeze quantification, similar to hybrid logic binders, binding variables to the current time, e.g.: \(Gx. (p \to Fy. (q \land y\leq x+3)).\)
  • time variables and quantification: \(\forall x G(p \land t=x \to F(q \land t\leq x+3)).\)

Each of the above formulae mean that “whenever in the future \(p\) holds, \(q\) will hold within 3 time units later”.

Such real-time extensions are usually very expressive and often lead to logics with undecidable decision problems. A way to regain decidability is to relax “punctuality” requirements involving precise time durations, by requirements involving time intervals. For further details see Alur and Henzinger (1992; 1993; 1994), as well as Reynolds (2010; 2014) on the real-time linear temporal logic RTL and the survey Konur (2013).

7.3 Quantified propositional temporal logics

Propositional temporal logics can be extended with quantifiers over atomic propositions, see Rescher and Urquhart (1971, Chapter XIX). Semantically, these quantify over all valuations of the atomic propositions, so they are monadic second-order quantifiers. The resulting languages are very expressive and the respective logics are usually undecidable, often not even recursively axiomatizable. Notable extensions include QPTL, the propositionally quantified extension of LTL, which is decidable, though with non-elementary complexity, as well as CTL* under some special semantic restrictions, see French (2001). Some complete axiomatic systems for quantified propositional temporal logics have been designed, see Kesten and Pnueli (2002) and French and Reynolds (2002) for QPTL with and without past operators, also providing proofs of decidability.

8. Combining temporal and other logics

Logics are often used to reason about dynamically changing structures or aspects of the world. It is therefore very natural to consider the evolution over time of such structures by adding a temporal dimension to them. An alternative perspective is to consider an instant-based model of time and associate with every instant in it a “snapshot” of the model at that time instant. This leads to the idea of adding a temporal dimension to a logic designed to reason about such models, that is to enrich the logical language with temporal operators suitable for reasoning about the evolution of the models over time. A prime example is first-order temporal logic, discussed in Section 8.1. Various modal logics can also be naturally temporalized and the relations between time and modality is one of the central questions in the philosophical study of modal logic. The study of historical necessity is another important example of philosophical analysis of a modality from temporal logic perspective. For philosophical and technical discussions on combining tenses and modalities see Rescher and Urquhart (1971, Chapters XII, XV, XX), Thomason (1984), Cocciarella (2006) and Lindström and Segerberg (2006).

From a technical viewpoint, there are several ways of combining models and logical systems and, in particular, of temporalising a logic: products, fusions, etc. (see the SEP entry on combining logics).

Some generic questions of transfer of logical properties, such as axiomatisations, completeness, decidability, etc. arise naturally. Decidability, for instance, is usually preserved in fusions, while it is often lost in products of logical systems. For general discussion and study of temporalizing logical systems and properties of temporised logics, see Finger and Gabbay (1992; 1996), Finger et al. (2002), Gabbay et al. (2003). Here we only briefly present and discuss some of the most popular cases of temporalized logical systems.

8.1 First-order temporal logics

Temporal Logic is obtained by adding the tense operators to an existing logic; above this was tacitly assumed to be the classical Propositional Calculus. Other temporal-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

\({\exists x(Philosopher(x)} \amp F King(x))\)
Someone who is now a philosopher will be a king at some future time.

\({\exists x F (Philosopher(x)} \amp King(x))\)
There now exists someone who will at some future time be both a philosopher and a king.

\({F \exists x(Philosopher(x)} \amp F King(x))\)
There will exist someone who is a philosopher and later will be a king.

\({F \exists x(Philosopher(x)} \amp King(x))\)
There will exist someone who is at the same time both a philosopher and a king.

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, it will be necessary to introduce in the semantics 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”.

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

\(F \exists {x}{Q}({x})\rightarrow \exists {x}F {Q}({x})\)
If there will be something that is \(Q,\) then there is now something that will be \(Q.\)

This formula can only be guaranteed to be true if there is a constant domain for all time instants; under this assumption, bare existence (as expressed by the existential quantifier) will need to be supplemented by a temporally restricted existence predicate (which might be read ‘is extant’) in order to refer to different objects existing at different times. For more on this and related problems of first-order temporal logics, see Chapter XX of Rescher and Urquhart (1971), Section 7 of van Benthem (1995) as well as Lindström and Segerberg (2006).

A related issue, particularly manifesting itself when combined with temporal reasoning, is the problem of definite descriptions: terms describing individuals, such as “the Pope”, “the present Pope”, and “Jorge Mario Bergoglio”, may or may not refer to the same (or to any) individual at different time instants, and the statements “the present Pope is from Argentina” and “Jorge Mario Bergoglio is from Argentina” have quite different truth behaviour over time. Even more problematic are description terms like “the present king of France” and an unquestionable semantics of the (true) statement that “the present king of France does not exists” is not easy to provide. See more on Russell’s theory of descriptions in the SEP entry Descriptions and on the relations with temporal reasoning and logics in Rescher and Urquhart (1971, Chapters XIII and XX).

Temporal first-order logics are typically highly undecidable. Few axiomatizable, and even fewer decidable, natural fragments of first-order temporal logics have been identified and investigated so far, including notably the monodic fragment, see Hodkinson et al. (2000) and Wolter and Zakharyaschev (2002).

8.2 Temporal-epistemic logics

Temporal-epistemic logics combine temporal and (multi-agent) logics of knowledge. Some natural properties can be expressed by combining temporal operators and the epistemic modality \(K\) (“it is known that”), e.g. perfect recall, or no forgetting: (If the agent knows \(p\) now then the agent will always know \(p\) in the future): \(K p \to GK p;\) and likewise no learning: \(FK p \to K p,\) etc. These were developed in various ways during the 1980s, with a unifying study by Halpern and Vardi (1989), who considered a variety of 96 temporal-epistemic logics with semantics based on so-called interpreted systems: sets of runs in a transition system with epistemic indistinguishability relations on the state space for each agent. The variety is based on six parameters: number of agents (one or many), the language (with or without common knowledge, linear or branching time, etc.), recall abilities (no recall, bounded recall, perfect recall), learning abilities (learning or no learning), synchrony (synchronous or asynchronous), unique initial state. Depending on the choice of these, the computational complexity of the decision problem for these logics ranges very broadly, from PSPACE-complete to highly undecidable (\(\Pi^{1}_{1}\)-complete). For further detail see Halpern and Vardi (1989), Fagin et al. (1995), as well as the more recent van Benthem and Pacuit (2006) which surveys a number of decidablity and undecidablity results concerning temporal-epistemic logics and illustrates again the crucial effect on the computational complexity which the combination of temporal and other modalities can bring about.

8.3 Temporal logics and logics of agency

Temporal reasoning is an important aspect of reasoning about agency. One of the most influential families of logics for agency originates from the work of Belnap and Perloff (1988), who introduced the operator “seeing to it that”, abbreviated stit, to reason about what agents can achieve by making suitable choices over time. Even though the original logics for stit do not involve time explicitly, their semantics is based on branching time models, where every agent’s set of choices at a given time instant is represented by a partition of the bunch of all histories passing through that instant. The formula \(\textit{stit}\, \varphi\) intuitively says that the agent can make a suitable choice such that all histories in that choice satisfy the objective \(\varphi.\) A number of extensions and elaborations of STIT logics have been subsequently developed Belnap et al. (2001). In particular, a temporal dimension has gradually been introduced explicitly into the STIT models and logics; for a recent account see Lorrini (2013), which gives formal semantics and complete axiomatisations of temporal STIT logics.

Another important family of temporal logics of agency are the multi-agent extensions of the branching time temporal logics CTL and CTL*, introduced in Alur et al. (2002) for temporal reasoning about open systems under the name alternating-time temporal logics ATL and ATL*. They have subsequently become a very popular logical framework for strategic reasoning in multiagent systems. These add to the language of LTL “strategic path quantifiers”, parameterised with sets of agents \(C\) and quantifying existentially over the collective strategies of \(C\) and then universally over the possible plays (histories) that can arise as a result of \(C\) following the chosen collective strategy. Thus, the main new syntactic construct in the logic ATL* is a formula of the type \(\langle\!\langle C \rangle\!\rangle \varphi,\) intuitively saying “The coalition \(C\) has a collective strategy to guarantee the satisfaction of the objective \(\varphi\) on every play (path) enabled by that collective strategy of \(C\)”. Here the objective \(\varphi\) is a temporal formula, specified for instance in the logic LTL. So, the one-step single-agent strategic operator in ATL is technically very similar to the stit operator of (Belnap and Perloff, 1988). The main technical difference between these logics is in the semantics, which is rather more general and abstract in the case of STIT, where ‘histories’ are abstract entities rather than concrete ‘plays’ – sequences of successor states generated by discrete transitions caused by collective actions of all agents, underlying the semantics of ATL. An extension of ATL, introducing some ideas from the STIT theory, was developed in Broersen et al. (2006).

ATL* naturally combines temporal and strategic reasoning in discrete multi-player games. The branching time logics CTL and CTL* can be regarded as single-agent versions of ATL and ATL*. Even though the latter are quite more expressive languages, they generally preserving the good computational properties of the former. For further details see Alur et al. (2002), as well as Goranko and van Drimmelen (2006), where a complete axiomatisation and decidability of ATL have been established.

8.4 Spatial-temporal logics

Space and time are intimately related in the physical world, and have become inseparable in modern physical theories. Combined logical reasoning about space-time has been actively evolving over the past decades, particularly in the context of Artificial Intelligence, spatio-temporal databases, ontologies and constraint networks. The main focus of recent research is on logical characterisation of spatio-temporal models, expressiveness and computational complexity Kontchakov et al. (2007). Another line of active recent research on logical theories for space-time is in the context of Relativity Theory (Andréka et al. 2007).

8.5 Temporal description logics

Description logics are very close to modal logics. They involve concepts (unary predicates) and roles (binary predicates) and are used to describe various ontologies and the relations between concepts in them. For further detail see e.g. Baader and Lutz (2006). Description logics can naturally be temporalized in various ways, see Artale and Franconi (2000), Wolter and Zakharyaschev (2000), and Lutz et al. (2008).

8.6 Temporal logics and other non-classical logics

Temporal logical reasoning can naturally be build on, or combined with, various non-classical logical systems resulting, for instance, in many-valued temporal logics (Rescher and Urquhart 1971, Chapter XVIII), intuitionistic temporal logics (Ewald 1986), constructive and paraconsistent temporal logics (Kamide and Wansing 2010; 2011), probabilistic temporal logics (Hart and Sharir 1986; Konur 2013), etc.

9. Logical deduction and decision methods for temporal logics

Extensive research and numerous publications over the past 50 years have developed a variety of logical deduction systems and decision methods for the temporal logics mentioned here and many more. Hilbert style axiomatic systems have been the most commonly developed logical deduction systems for temporal logics. Besides, many complete systems of semantic tableaux, sequent calculi, and resolution-based systems have been developed for various temporal logics. It is beyond the scope and space of this entry to provide any comprehensive account of these, so here we only list some general references on deductive systems for temporal logics, in addition to the more specific references mentioned elsewhere in this text: Rescher and Urquhart (1971), Burgess (1984), Goldblatt (1987), Emerson (1990), Gabbay et al. (1994), Bolc and Szalas (1995), van Benthem (1995), Gabbay and Guenthner (2002), Gabbay et al. (2003), Fisher et al. (2005), Blackburn et al. (2006), Kröger and Merz (2008), Fisher (2011).

Particularly efficient and practically useful are the tableaux-based methods for deciding satisfiability. The method of semantic (aka, analytic) tableaux, originating from pioneering work of Beth, Hintikka, Smullyan, and Fitting, is based on a systematic search of satisfying model (reap., falsifying counter-model) if an input formula which is tested for satisfiability (reap., validity), which is guaranteed to be able to find such model whenever it exists. It has been successfully developed for constructive satisfiability testing for a variety of temporal logics, see Goré (1999) for a survey on tableaux systems for many temporal logics and more specifically: Ben-Ari et al. (1983) for the branching time logic UB; Wolper (1985) for the linear time logic LTL; Emerson and Halpern (1985) for the computation tree logic CTL, Reynolds (2007) for CTL with bundled trees semantics; Goranko and Shkatov (2010) for ATL; Reynolds (2011) for the full computation tree logic CTL*; Reynolds (2014) for the real-time temporal logic RTL, etc.

Other very important and practically useful are the automata-based methods, used both for deciding satisfiability and for model checking of temporal logics. These methods have been actively developing since the early 1990s. They are based on classical results about decidability of the monadic 2nd order theories of the natural numbers (by Büchi) and of the infinite binary tree (by Rabin). The automata-based methods transform temporal formulae into automata on infinite words (for linear time logics) or infinite trees (for branching time logics) and represent models for the logics as respective input objects (infinite words or trees) for their associated automata. Thus, in particular, satisfiability of a formula becomes equivalent to non-emptiness of the language of the automaton associated with that formula. For instance, automata on infinite trees and Rabin’s theorem were used to obtain a decision procedure for CTL* in Emerson and Sistla (1984). For further details see Vardi (2006).

Other important references on decidability results and decision procedures for various temporal logics include Burgess (1980) and Gurevich and Shelah (1985) for branching time logics, Burgess and Gurevich (1985) for linear temporal logics, Goldblatt (1987) on both linear and branching time logics, Montanari and Policriti (1996) on metric and layered temporal logics, French (2001) for some quantified propositional branching time logics.

While most propositional temporal logics are decidable, adding some syntactic or semantic features can make them explode computationally and become undecidable. Many important extended temporal logics become generally undecidable, even under very weak assumptions. Besides combinations with other very expressive logics, discussed in Section 8, other most common causes of undecidability in temporal logics include: grid-like models, typical for many-dimensional or temporalized systems; temporal operators along multiple time-lines; products of temporal logics; interval-based logics, where truth of formulae is defined on time intervals with no locality assumptions; time reference mechanisms, such as freeze quantifiers and hybrid binders; arithmetic features: time addition, exact time constraints, etc. However, there are various ways to tame temporal logics and restore decidability, such as: syntactic restrictions, identifying decidable fragments (e.g. the two-variable fragment of classical first-order logic FO\(^{2},\) guarded fragments, monodic fragments, etc.); suitable parametric restrictions, e.g. on the number of propositional variables or the depth of nesting; suitable semantic restrictions, e.g., locality for interval logics, etc.

10. Applications of temporal logics

Temporal logic is one of the most broadly applicable areas of logic and philosophy, with actual or potential applications ranging from computer science, artificial intelligence and linguistics, to natural, cognitive, and social sciences. In this entry we will restrict ourselves to very brief expositions of some of these.

10.1 Temporal logics in Computer Science

Temporal logic is one of the natural meeting points of philosophy and computer science, whose separate issues and agendas come together here in a fertile interaction. Early work implicitly suggesting applications of temporal reasoning to modelling and analysis of deterministic and stochastic transition systems is the theory of processes and events in Rescher and Urquhart (1971, Chapter XIV). However, temporal logic became really prominent in Computer Science with the seminal paper of Pnueli (1977) who proposed application of temporal logics to specification and verification of reactive and concurrent programs and systems. In order to ensure correct behaviour of a reactive program, in which computations are non-terminating (e.g., an operating system) it is necessary to formally specify and verify the acceptable infinite executions of that program. Likewise, to ensure correctness of a concurrent program, performed by two or more processors working in parallel, it is necessary to formally specify and verify their synchronization, i.e., the way in which the actions of the various processors are interrelated, and to formally describe the acceptable infinite executions of the program. 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.

Key temporal patterns of importance in specifying such programs are:

  • “liveness” properties, or “eventualities”, involving temporal patterns \(F {p},\) \(q \to F {p},\) or \(G(q \to F {p}),\) which ensure that if a specific precondition (\(q\)) is initially satisfied, then a desirable state (satisfying \(p\)) will eventually be reached in the course of the computation. For example, such are “If a message is sent, eventually it will be delivered” and “Whenever a printing job is activated, eventually it will be completed”.
  • “safety” or “invariance” properties, involving temporal patterns \({G} {p},\) \(q \to {G} {p},\) or \(G(q \to {G} {p}),\) which ensure that if a specific precondition (\(q\)) is initially satisfied, then undesirable states (violating the safety condition \(p\)) will never occur. Examples are: “No more than one process will be in its critical section at any moment of time”, “A resource will never be used by two or more processes simultaneously”, or, for more practical examples: “The traffic lights will never show green in both directions”, “A train will never pass a red semaphore”.
  • “fairness” properties, involving combinations of temporal patterns of the form \({GF} {p}\) (“infinitely often \(p\)”) or \({FG} {p}\) (“eventually always \(p\)”). Intuitively, fairness requires that in a system where several processes sharing resources are run concurrently, they must be treated ‘fairly’ by the operating system, scheduler, etc. A typical fairness requirement says that if a process is persistent enough in sending a request (e.g., keeps sending it over and over again) then eventually its request will be granted.

Since infinite computations are formally represented by models of the linear time logic LTL, while non-determinism modelled by branching time is an inherent feature of many computer science applications, both LTL and the computation tree logics CTL and CTL* have been very important for specification and verification of concurrent and reactive systems. Here is an example combining liveness and safety properties of a single computation: “Whenever a state of alert is reached, the alarm is activated and remains activated until a safe state is eventually reached”. It is expressible in LTL as

\[ G(\tt{alert} \to (\tt{alarm} \ U\ \tt{safe})). \]

Another example, referring to all computations in the system: “If the process \(\sigma\) is eventually enabled on some computation starting from the current state, then on every computation starting there, whenever \(\sigma\) is enabled it will remain enabled until the process \(\tau\) is disabled” can be formalised in CTL* as:

\[ \Diamond F\,\textsf{enabled}_{\sigma} \to \Box G(\textsf{enabled}_{\sigma} \to (\textsf{enabled}_{\sigma} \,U\, \textsf{disabled}_{\tau})). \]

A variation of LTL with useful applications for specifying and reasoning about concurrent systems is Lamport’s (1994) temporal logic of actions TLA. Other applications of temporal logics in computer science include: temporal databases, real-time processes and systems, hardware verification, etc. Further information on such applications may be found e.g., in Pnueli (1977), Emerson and Clarke (1982), Moszkowski (1983), Galton (1987), Emerson (1990), Alur and Henzinger (1992), Lamport (1994), Vardi and Wolper (1994), Bolc and Szalas (1995), Kröger and Merz (2008), Fisher (2011).

10.2 Temporal logics in Artificial Intelligence

Relating temporal reasoning to Artificial Intelligence (AI) goes back at least to the already mentioned theory of processes and events in Rescher and Urquhart (1971, Chapter XIV). Temporal representation and reasoning has been a more prominent theme in AI since the seminal work of Allen (1984), mentioned in the context of interval temporal logics, which is concerned with finding a general framework adequate for all 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. Temporal reasoning has also been naturally combined with other well-developed frameworks for AI, such as the Situation Calculus (Pinto and Reiter 1995) and Action Theory (Lamport 1994). A useful survey of issues involving time and temporal reasoning in AI is Galton (1995); more recent surveys of the area are Fisher et al. (2005) and the more concise handbook chapter (Fisher 2008).

An issue that has loomed large in the context of AI — but which is also important for both philosophy and linguistics — concerns the logical form of statements involving time or tense. Perhaps the most traditional approach is by way of the so-called method of temporal arguments, in which 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 example

\[ \text{Kill}(\text{Brutus}, \text{Caesar}, 44\text{BCE}). \]

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

The method of temporal arguments encounters difficulties, however, 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 Allen (1984). 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))
Occurs(Walk-to(John, Station), (1pm, 1.15pm))

where terms of the form \(({t}, t')\) denote time intervals in the obvious way.

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

\(\forall {s}, {i}, {i'} (Holds({s}, {i}) \land In( {i'}, {i}) \rightarrow Holds({s}, {i'}))\)
\(\forall {e}, {i}, {i'}(Occurs({e}, {i}) \land In( {i'}, {i}) \rightarrow \neg Occurs({e}, {i'}))\)

where “\(In\)” expresses the proper subinterval relation.

An alternative to reifying event types is to reify event tokens. This idea 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 as

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

The 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

\(\exists {e}(See(John, Mary, {e}) \& Place({e}, London) \land Time({e}, Tuesday)),\)
Therefore, \(\exists {e}(See(John, Mary, {e}) \land Time({e}, Tuesday)).\)

In this form, the inference does not require any 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 been used in a computational context in the Event Calculus of Kowalski and Sergot (1986).

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 an 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 so 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 reference for the frame problem is Shanahan (1997.

10.3 Temporality in natural language and linguistics

Temporal aspects of natural languages are diverse and pervasive. One of the first analytic approaches to that topic, listed in Prior (1967) amongst the precursors of Tense Logic, was 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 triple of time points related to the utterance, namely: the speech time \(S,\) the reference time \(R,\) and the event time \(E.\) With that theory Reichenbach characterized most of the tenses in natural language. For instance, he was neatly able to distinguish between the simple past “I saw John”, for which \(E=R \lt S,\) and the present perfect “I have seen John”, for which \(E \lt R=S,\) the former statement referring to a past time coincident with the event of seeing John, the latter to the present time, relative to which the seeing of John is in the past. Still, 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 logics presented here. For some examples, see Dowty (1979), Galton (1984), Taylor (1985), Richards et al. (1989). A useful collection of landmark papers in this area is Mani et al. (2005). For further detail see Steedman (1997), Kuhn and Portner (2006), and the entry on tense and aspect.

Bibliography

  • Allen, J.F., 1983, “Maintaining knowledge about temporal intervals”, Communications of the ACM, 26(11): 832–843.
  • –––, 1984, “Towards a general theory of action and time”, Artificial Intelligence, 23: 123–154.
  • Alur, R. and Henzinger, T., 1992, “Logics and models of real-time: a survey”, in Real-Time: Theory in Practice: Proceedings of the REX Workshop, 1991 (Lecture Notes in Computer Science: Volume 600), Berlin: Springer, 74–106.
  • –––, 1993, “Real-time logics: Complexity and expressiveness”, Information and Computation, 104: 35–77.
  • –––, 1994, “A really temporal logic”, Journal of the ACM, 41: 181–204.
  • Alur, R. Henzinger, T. and Kupferman, O., 2002, “Alternating-time temporal logic”, Journal of the ACM, 49(5): 672–713.
  • Andréka, H., Goranko, V., Mikulas, S. Németi, I. and Sain, I., 1995, “Effective first-order temporal logics of programs”, in Bolc and Szalas (1995), pp. 51–129.
  • Andréka, H., Madar’sz, J. and Németi, I., 2007, “Logic of Space-Time and Relativity Theory”, chapter in M. Aiello, J. van Benthem and I. Pratt-Hartmann (eds), Handbook of Spatial Logics, Dordrecht: Springer 2007, pp. 607–711.
  • Areces, C., and ten Cate, B., 2006, “Hybrid Logics”, in Blackburn et al. (2006), pp. 821–868.
  • Aristotle, Organon, II - On Interpretation, ch.9. See   https://archive.org/stream/AristotleOrganon/AristotleOrganoncollectedWorks.
  • Artale, A. and Franconi, E., 2000, “A survey of temporal extensions of description logics”, Annals of Math. and AI, 30: 171–210.
  • Baader, F. and Lutz, C., 2006, “Description Logic”, chapter in Blackburn et al. (2006), pp. 757–819.
  • Balbiani, P., Goranko, V. and Sciavicco, G., 2011, “Two-sorted Point-Interval Temporal logics”, in Proc. of the 7th International Workshop on Methods for Modalities (M4M7) (Electronic Notes in Theoretical Computer Science: Volume 278), pp. 31–45.
  • Belnap, N. and Green, M., 1994, “Indeterminism and the Thin Red Line”, in Philosophical Perspectives (Volume 8: Logic and Language), Atascadero, CA: Ridgeview, pp. 365–388.
  • Belnap, N. and Perloff, M., 1988, “Seeing to it that: A canonical form for agentives”, Theoria, volume 54, pp. 175–199, reprinted with corrections in H. E. Kyberg et al. (eds.), Knowledge Representation and Defeasible Reasoning, Dordrecht: Kluwer, 1990, pp. 167–190.
  • Belnap, N., Perloff, M., and Xu, M., 2001, Facing the future: Agents and choice in our indeterminist world, Oxford: Oxford University Press.
  • Ben-Ari, M., Pnueli, A. and Manna, Z., 1983, “The temporal logic of branching time”, Acta Informatica, 20(3): 207–226.
  • van Benthem, J., 1983, The Logic of Time, Dordrecht, Boston and London: Kluwer Academic Publishers. [Second edition: 1991.]
  • –––, 1995, “Temporal Logic”, in D.M. Gabbay, C.J. Hogger, and J.A. Robinson (eds.), Handbook of Logic in Artificial Intelligence and Logic Programming (Volume 4), Oxford: Clarendon Press, pp. 241–350.
  • van Benthem, J., and ter Meulen, A., (editors), 1997, Handbook of Logic and Language, Amsterdam: Elsevier.
  • van Benthem, J., and E. Pacuit, 2006, “The Tree of Knowledge in Action: Towards a Common Perspective”, in Advances in Modal Logic (Volume 6), London: College Publications, pp. 87–106.
  • Blackburn, P., 2006, “Arthur Prior and Hybrid Logic”, Synthese, 150: 329–372.
  • Blackburn, P., van Benthem, J, and Wolter, F., 2006, Handbook of Modal Logics, Amsterdam: Elsevier.
  • Bolc, L. and Szalas, A. (eds.), 1995, Time and Logic: A Computational Approach, London: UCL Press.
  • Boyd, S., 2014, “Defending History: Temporal Reasoning in Genesis 2:7–3:8”, Answers Research Journal, 7: 215–237.
  • Bresolin, D., Goranko, V., Montanari, A. and Sciavicco, G., 2009, “Propositional Interval Neighborhood Logics: Expressiveness, Decidability, and Undecidable Extensions”, Annals of Pure and Applied Logic, 161(3): 289–304.
  • Bresolin, D., Della Monica, D., Goranko, V., Montanari, A. and Sciavicco, G., 2013, “Metric propositional neighborhood logics on natural numbers”, Software and Systems Modeling, 12(2): 245–264.
  • Broersen, J., Herzig, A. and Troquard, N., 2006, “A STIT-extension of ATL”, in Proc. of JELIA’2006, LNAI 4160, Berlin: Springer, pp. 69–81.
  • Brown, M., and Goranko, V., 1999, “An extended branching-time Ockhamist temporal logic”, Journal of Logic, Language and Information, 8(2): 143–166.
  • Bull, R., 1970, “An approach to tense logic”, Theoria, 36: 282–300.
  • Burgess, J., 1979, “Logic and time”, Journal of Symbolic Logic, 44: 566–582.
  • Burgess, J., 1980, “Decidability for branching time”, Studia Logica, 39: 203–218.
  • Burgess, J., 1982a, “Axioms for tense logic I: ‘Since’ and ‘Until’”, Notre Dame Journal of Formal Logic, 23: 367–374.
  • Burgess, J., 1982b, “Axioms for tense logic II: Time Periods”, Notre Dame Journal of Formal Logic, 23: 375–383.
  • Burgess, J., 1984, “Basic tense logic”, in Gabbay and Guenthner (eds.), Handbook of Philosophical Logic (Volume 2), Dordrecht: Reidel, pp. 89–133. [New edition in Gabbay and Guenthner (2002), pp. 1–42.]
  • Burgess, J. and Gurevich, Y., 1985, “The decision problem for linear temporal logic”. Notre Dame Journal of Formal Logic, 26(2): 115–128.
  • Ciuni, R., and Zanardo, A., 2010, “Completeness of a Branching-Time Logic with Possible Choices”, Studia Logica, 96: 393–420.
  • Cocchiarella, N., 2002, “Philosophical Perspectives on Quantification in Tense and Modal Logic”, in Gabbay & Guenthner (2002), pp. 235–276.
  • Della Monica, D., Goranko, V., Montanari, A., Sciavicco, G., 2011, “Interval Temporal Logics: A Journey”, Bulletin of the European Association for Theoretical Computer Science, 105: 73–99.
  • Davidson, D., 1967, “The Logical Form of Action Sentences”, in N. Rescher (ed.), The Logic of Decision and Action, Pittsburgh: University of Pittsburgh Press, 1967, pp. 81–95. [Reprinted in D. Davidson, Essays on Actions and Events, Oxford: Clarendon Press, 1990, pp. 105–122.]
  • Dowty, D., 1979, Word Meaning and Montague Grammar, Dordrecht: Reidel.
  • Emerson, E.A. and E. C. Clarke, 1982, “Using branching time temporal logic to synthesise synchronisation skeletons”, Science of Computer Programming, 2: 241–266.
  • Emerson, E.A. and J. Halpern, 1985, “Decision procedures and expressiveness in the temporal logic of branching time”, Journal of Computer and Systems Science, 30: 1–24.
  • Emerson, E.A. and Sistla, A., 1984, “Deciding full branching time logic”, Information and Control, 61: 175–201.
  • Emerson, E.A., 1990, “Temporal and modal logics”, in J. van Leeuwen, (ed.), Handbook of Theoretical Computer Science, volume B: Formal Models and Semantics, Amsterdam: Elsevier, pp. 995–1072.
  • Ewald, W., 1986, “Intuitionistic Tense and Modal Logic”, Journal of Symbolic Logic, 51(1): 166–179.
  • Fagin, R., Halpern, J., Moses, Y., and Vardi, M., 1995, Reasoning about Knowledge, Boston: The MIT Press.
  • Fine, K., 1970, “Propositional quantifiers in modal logic”, Theoria, 36: 336–346.
  • Finger, M. and Gabbay, D., 1992, “Adding a temporal dimension to a logic system”, Journal of Logic, Language and Information, 1(3): 203–233.
  • Finger, M. and Gabbay, D., 1996, “Combining Temporal Logic Systems”, Notre Dame Journal of Formal Logic, 37(2): 204–232.
  • Finger, M. and Gabbay, D. and Reynolds. M., 2002, “Advanced tense logic”, in Gabbay and Guenthner (2002), pp. 43–204.
  • Fisher, M., Gabbay, D., and Vila, L., 2005, Handbook of Temporal Reasoning in Artificial Intelligence, Amsterdam: Elsevier.
  • Fisher, M., 2008, “Temporal Representation and Reasoning”, in F. van Harmelen, V. Lifschitz and B. Porter (eds.), Handbook of Knowledge Representation, Amsterdam: Elsevier, pp. 513–550.
  • Fisher, M., 2011, An Introduction to Practical Formal Methods Using Temporal Logic, Somerset, NJ: Wiley.
  • French, T., 2001, “Decidability of Quantified Propositional Branching Time Logics”, Advances in AI (Lecture Notes in Computer Science: Volume 2256), Berlin: Springer, pp. 165–176.
  • French, T. and Reynolds, M., 2002, “A Sound and Complete Proof System for QPTL”, Advances in Modal Logic, 4: 127–148.
  • Gabbay, D.M. and Guenthner, F. (editors), 2002, Handbook of Philosophical Logic (Volume 7), second edition, Dordrecht: Kluwer.
  • Gabbay, D. M., Hodkinson, I., and Reynolds, M., 1994, Temporal Logic: Mathematical Foundations and Computational Aspects, Volume 1, Oxford: Clarendon Press.
  • Gabbay, D. M., Reynolds, M. and Finger, M., 2000, Temporal Logic: Mathematical Foundations and Computational Aspects (Volume 2), Oxford: Oxford University Press.
  • Gabbay, D., Kurucz, A., Wolter, F., and Zakharyaschev, M., 2003, Many-dimensional modal logics: theory and applications, Amsterdam: Elsevier.
  • Galton, A. P., 1984, The Logic of Aspect, Oxford: Clarendon Press.
  • –––, 1987, Temporal Logics and their Applications, London: Academic Press.
  • –––, 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, pp. 175–240.
  • Garson, J., 1984, “Quantification in modal logic”, in D. M. Gabbay and F. Guenthner (eds.), Handbook of Philosophical Logic, Dordrecht: D. Rediel, pp. 249–307.
  • Goldblatt, R., 1980, “Diodorean Modality in Minkowski Spacetime”, Studia Logica, 39: 219–236. Reprinted in Mathematics of Modality (CSLI Lecture Notes 43), Stanford: CSLI Publications, 1993.
  • –––, 1987, Logics of Time and Computation (CSLI Lecture Notes 7), Stanford: CSLI Publications; second edition, 1992.
  • Goranko, V., 1996, “Hierarchies of modal and temporal logics with reference pointers”, J. of Logic, Language and Information, 5(1): 1–24.
  • Goranko, V., Montanari, A. and Sciavicco, G., 2003, “Propositional Interval Neighborhood Logics”, Journal of Universal Computer Science, 9(9): 1137–1167.
  • –––, 2004, “A Road Map of Propositional Interval Temporal Logics and Duration Calculi”, Journal of Applied Non-classical Logics (Special issue on Interval Temporal Logics and Duration Calculi), 14(1–2): 11–56.
  • Goranko, V. and van Drimmelen, G., 2006, “Complete axiomatization and decidablity of the alternating-time temporal logic”, Theoretical Computer Science, 353: 93–117.
  • Goranko, V. and Shkatov, D., 2010, “Tableau-based decision procedures for logics of strategic ability in multi-agent systems”, ACM Transactions of Computational Logic, 11(1): 3:1–3:51.
  • Goré, R., 1999, “Tableau methods for modal and temporal logics”, in M. D’Agostino, D.M. Gabbay, R. Hahnle, and J. Posegga, (eds), Handbook of Tableau Methods, Dordrecht: Kluwer, pp. 297–396.
  • Gurevich, Y. and Shelah, S. 1985, “The decision problem for branching time logic”, Journal of Symbolic Logic, 50: 668–681.
  • Halpern, J. and Shoham, Y., 1986. “A propositional modal logic of time intervals”, in Proceedings of the 2nd IEEE Symposium on Logic in Computer Science, pp. 279–292; reprinted in Journal of the ACM, 38(4) (1991): 935–962.
  • Halpern, J. and Vardi, M., 1989, “The complexity of reasoning about knowledge and time I: Lower bounds”, Journal of Computer and System Sciences, 38(1): 195–237.
  • Hamblin, C., 1971, “Instants and intervals ”, Studium Generale , 24: 127–134.
  • Hansen, M.R., and Zhou C., 1997, “Duration Calculus: Logical Foundations” Formal Aspects of Computing, 9: 283–330.
  • Hart, S. and Sharir, M., 1986, “Probabilistic Propositional Temporal Logics”, Information and Control, 70(2/3): 97–155.
  • Hodkinson, I., Wolter F., and Zakharyaschev, M., 2000, “Decidable fragment of first-order temporal logics”, Ann. Pure Appl. Logic, 106(1–3): 85–134.
  • Hodkinson, I. and Reynolds, M., 2006, “Temporal Logic”, in Blackburn et al. (2006), pp. 655–720.
  • Humberstone, I.L., 1979, “Interval Semantics for Tense Logic: Some Remarks”, Journal of Philosophical Logic, 8: 171–196.
  • Kamide, N. and Wansing, H., 2010, “Combining linear-time temporal logic with constructiveness and paraconsistency”, Journal of Applied Logic, 6: 33–61.
  • Kamide, N. and Wansing, H., 2011, “A paraconsistent linear-time temporal logic”, Fundamenta Informaticae, 106: 1–23.
  • Kamp, J., 1968. Tense Logic and the Theory of Linear Order, Ph.D. thesis, University of California, Los Angeles.
  • –––, 1971, “Formal properties of ‘Now’”, Theoria, 37: 227–273.
  • Kesten, Y. and Pnueli, A., 2002, “Complete Proof System for QPTL”. Journal of Logic and Computation, 12(5): 701–745.
  • Kontchakov, R., Kurucz, A., Wolter, F. and Zakharyaschev, M., 2007, “Spatial Logic + Temporal Logic = ?”, chapter in M. Aiello, J. van Benthem and I. Pratt-Hartmann (eds), Handbook of Spatial Logics, Berlin: Springer, pp. 497–564.
  • Konur, S., 2013, “A survey on temporal logics for specifying and verifying real-time systems”, Frontiers of Computer Science, 7(3): 370–403.
  • Koymans, R., 1990, “Specifying real-time properties with metric temporal logic”, Real-time Systems, 2(4): 255–299.
  • Kowalski, R. A. and Sergot, M. J., 1986, “A Logic-Based Calculus of Events”, New Generation Computing, 4: 67–95.
  • Kröger, F. and Merz. S., 2008, Temporal Logic and State Systems (EATCS Texts in Theoretical Computer Science Series), Berlin: Springer.
  • Kuhn, S.T. and Portner, P, 2006, “Tense and Time”, in Gabbay and Guenthner (2002), pp. 277–346.
  • Ladkin, P,. 1987, The Logic of Time Representation, Ph.D. thesis, University of California, Berkeley.
  • Lamport, L, 1994, “The temporal logic of actions”, J. ACM Transactions on Prog. Languages and Systems, 16(3): 872–923.
  • Lindström, S. and Segerberg, K., 2006, “Modal logic and philosophy”, chapter in Blackburn et al. (2006), pp. 1149–1214
  • Lorrini, E., 2013, “Temporal STIT logic and its application to normative reasoning”, Journal of Applied Non-Classical Logics, 23(4): 372–399.
  • Lutz, K., Wolter, F. and Zakharyaschev, M., 2008, “Temporal Description Logics: A Survey”, Proceedings of TIME 2008, pp. 3–14.
  • Manna, Z. and Pnueli, 1992, A. The Temporal Logic of Reactive and Concurrent Systems (Volume 1: Specifications), Springer: New York.
  • Mani, I., Pustejovsky, J., and Gaizauskas, R., 2005, The Language of Time: A Reader, Oxford: Oxford University Press.
  • Marx, M. and Reynolds, M., 1999, “Undecidability of compass logic”, Journal of Logic and Computation, 9(6): 897–914.
  • Massey, G., 1969, “Tense Logic! Why Bother?”, Noûs, 3: 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 UP, pp. 463–502.
  • Mellor, D. H., 1981, Real Time, Cambridge: Cambridge UP; Chapter 6 reprinted with revisions as “The Unreality of Tense”, in R. Le Poidevin and M. MacBeath (eds.), The Philosophy of Time, Oxford: Oxford University Press, 1993.
  • Montanari, A., 1996, Metric and Layered Temporal Logic for Time Granularity (Institute for Logic, Language, and Computation Dissertation Series, Number 1996–02), Amsterdam: University of Amsterdam.
  • Montanari, A. and Policriti, A., 1996, “Decidability Results for Metric and Layered Temporal Logics”, Notre Dame Journal Formal Logic, 37(2): 260–282.
  • Moszkowski, B., 1983, Reasoning about digital circuits, Ph.D. Thesis (Technical Report STAN-CS-83–970), Department of Computer Science, Stanford University.
  • Øhrstrøm, P. and Hasle, P., 1995, Temporal Logic: From Ancient Ideas to Artificial Intelligence, Dordrecht: Kluwer Academic Publishers.
  • Pinto, J. and Reiter, R., 1995, “Reasoning about time in the situation calculus”, Annals of Mathematics and Artificial Intelligence, 14(2–4): 251–268.
  • Pnueli, A., 1977, “The temporal logic of programs”, Proceedings of the 18th IEEE Symposium on Foundations of Computer Science, pp. 46–67.
  • Prior, A. N., 1957, Time and Modality, Oxford: Clarendon Press.
  • –––, 1967, Past, Present and Future, Oxford: Clarendon Press.
  • –––, 1969, Papers on Time and Tense, Oxford: Clarendon Press; new edition, P. Hasle et al. (eds.), Oxford: Oxford University Press, 2003.
  • Reichenbach, H., 1947, Elements of Symbolic Logic, New York: Macmillan.
  • Rescher, N. and Urquhart, A., 1971, Temporal Logic, Berlin: Springer-Verlag.
  • Reynolds, M., 2001, “An axiomatization of Full Computation Tree Logic”, Journal of Symbolic Logic, 66: 1011–1057.
  • –––, 2002, “Axioms for Branching Time”. Journal of Logic and Computation, 12(4): 679–697.
  • –––, 2003, “An Axiomatization of Prior’s Ockhamist Logic of Historical Necessity”, in Balbiani et al. (eds.), Advances in Modal Logic (Volume 4), pp. 355–370, London: College Publications
  • –––, 2005, “An axiomatization of PCTL*”, Information and Computation, 201(1): 72–119.
  • –––, 2007, “A Tableau for Bundled CTL”, Journal of Logic and Computation, 17(1): 117–132.
  • –––, 2010, “The complexity of temporal logic over the reals”, Annals of Pure and Applied Logic, 161(8): 1063–1096.
  • –––, 2011, “A tableau-based decision procedure for CTL*”, Formal Aspects of Computing, 23(6): 739–779.
  • –––, 2014, “A Tableau for Temporal Logic over the Reals”, in Advances in Modal Logic (Volume 10), London: College Publications, pp. 439–458.
  • Richards, B., Bethke, I., van der Does, J., and Oberlander, J., 1989, Temporal Representation and Inference, London: Academic Press.
  • Röper, P., 1980, “Intervals and tenses”, Journal of Philosophical Logic, 9: 451–469.
  • Shanahan, M., 1997, Solving the Frame Problem, Cambridge, MA and London: MIT Press.
  • Segerberg, K., 1970, “Modal logics with linear alternative relations”, Theoria, 36: 301–322.
  • Steedman, M., 1997, “Temporality”, in van Benthem and ter Meulen (1997), pp. 925–969.
  • Stirling, C., 1992, “Modal and temporal logics”, in Handbook of Logic in Computer Science: Volume 2 (Background: Computational Structures), Clarendon Press: Oxford, pp. 477–563.
  • Taylor, B., 1985, Modes of Occurrence: Verbs, Adverbs, and Events (Aristotelian Society Series: Volume 2), Oxford: Basil Blackwell.
  • Thomason, R., 1984, “Combinations of tense and modality”, in Handbook of Philosophical Logic (Volume II: Extensions of Classical Logic), D. Gabbay and F. Guenthner, eds, pp. 135–165. Reidel. New edition in Gabbay and Guenthner (2002), pp. 205–234.
  • Vardi, M., 2006, “Automata-theoretic techniques for temporal reasoning”, in Blackburn et al. (2006), pp. 971–989.
  • Vardi, M. and Wolper, P., 1994, “Reasoning about infinite computations”, Information and Computation, 115: 1–37.
  • Venema, Y., 1990, “Expressiveness and completeness of an interval tense logic”, Notre Dame Journal of Formal Logic, 31: 529–547.
  • –––, 1993, “Completeness via completeness: Since and Until”, in M. de Rijke (ed.), Diamonds and Defaults, Dordrecht: Kluwer, pp. 279–286.
  • –––, 1991, “A modal logic for chopping intervals”, Journal of Logic and Computation, 1(4): 453–476.
  • –––, 2001, “Temporal Logic”, in Lou Goble, ed., Blackwell Guide to Philosophical Logic, Oxford: Blackwell Publishers.
  • Wolper, P., 1985, “The tableau method for temporal logic: An overview”, Logique et Analyse, 110–111: 119–136.
  • Wolter F., and Zakharyaschev, M., 2000, “Temporalizing description logics”, in D. Gabbay and M. de Rijke (eds.), Frontiers of Combining Systems II, Chichester, NY: Research Studies Press/Wiley, pp. 379–401.
  • –––, 2002, “Axiomatizing the monodic fragment of first-order temporal logic”, Annals of Pure and Applied Logic, 118(1–2): 133–145.
  • Xu, M., 1995, “On the basic logic of STIT with a single agent”, Journal of Symbolic Logic, 60: 459–483.
  • –––, 1988, “On some U,S-tense logics”. Journal of Philosophical Logic, 17: 181–202.
  • Zanardo, A., 1985, “A finite axiomatization of the set of strongly valid Ockamist formulas”, Journal of Philosophical Logic, 14: 447–468.
  • –––, 1990, “Axiomatization of ‘Peircean’ branching-time logic”, Studia Logica, 49: 183–195.
  • –––, 1991, A complete deductive system for since-until branching time logic. Journal of Philosophical Logic, 20: 131–148.
  • –––, 1996, “Branching-time logic with quantification over branches: the point of view of modal logic”, Journal of Symbolic Logic, 61: 1–39.
  • Zanardo, A., Barcellan, B., and Reynolds, M., 1999, “Non-Definability of the Class of Complete Bundled Trees”, Logic Journal of the IGPL (Special Issue on Temporal Logic), 7(1): 125–136.

Acknowledgments

The authors would like to thank the anonymous reviewer, as well as Johan van Benthem, Rob Goldblatt, Angelo Montanari, Uri Nodelman, Yde Venema, Michael Zakharyaschev, Ed Zalta, and Alberto Zanardo for some helpful suggestions and corrections.

Copyright © 2015 by
Valentin Goranko <valentin.goranko@philosophy.su.se>
Antony Galton

This is a file in the archives of the Stanford Encyclopedia of Philosophy.
Please note that some links may no longer be functional.
[an error occurred while processing this directive]