Temporal Logics

Reading preferences

Optional display controls need JavaScript. All reading content and navigation work without it.

Editorial

This chapter covers temporal logics.

Introduction

Temporal logics deal with claims about things that will or have been the case. Arthur Prior is credited as the originator of temporal logic, which he called tense logic. Our treatment of temporal logic here will largely follow Prior's original modal treatment of introducing temporal operators into the basic framework of propositional logic, which treats claims as generally lacking in tense.

For example, in propositional logic, I might talk about a dog, Beezie, who sometimes sits and sometimes doesn't sit, as dogs are wont to do. It would be contradictory in classical logic to claim that Beezie is sitting and also that Beezie is not sitting. But obviously both can be true, just not at the same time; adding temporal operators to the language can allow us to express that claim relatively easily. The addition of temporal operators also allows us to account for the validity of inferences like the one from “Beezie will get a treat or a ball" to “Beezie will get a treat or Beezie will get a ball."

However, a lot of philosophical issues arise with temporal logic that might lead us to adopt one framework of temporal logic over another. For example, a future contingent is a statement about the future that is neither necessary nor impossible. If we say “Richard will go to the grocery store tomorrow," we are expressing a claim about something that has not yet happened, and whose truth value is contestable. In fact, it is contestable whether that claim can even be assigned a truth value in the first place. If we are strict determinists, then perhaps we can be comfortable with the idea that this sentence is in fact true or false, even before the event in question is supposed to take place---it just may be that we do not know its truth value yet. In contrast, we might believe in a genuinely open future, in which the truth values of future contingents are undetermined.

As it turns out, a lot of these commitments about the structure and nature of time are built in to our choices of models and frameworks of temporal logics. For example, we might ask ourselves whether we should construct models in which time is linear, branching or even circular. We might have to make decisions about whether our temporal models will have beginning and end points, and whether time is to be represented using discrete instants or as a continuum.

Semantics for Temporal Logic

Definition of the basic temporal language

The basic language of temporal logic contains

The propositional constant for falsity $\lfalse$ source.
A denumerables set of propositional variables: $\Obj p_0$ source, $\Obj p_1$ source, $\Obj p_2$ source, dots
The propositional connectives: $\lnot$ source (negation) , $\land$ source (conjunction) , $\lor$ source (disjunction) , $\lif$ source (conditional) .
Past operators $\Ptemp$ source and $\Htemp$ source.
Future operators $\Ftemp$ source and $\Gtemp$ source.

Later on, we will discuss the potential addition of other kinds of modal operators.

Inductive definition of temporal formulas

Formulas of the temporal language are inductively defined as follows:

$\lfalse$ source is an atomic formula.
Every propositional variable $\Obj p_i$ source is an (atomic) formula.
If $!A$ source is a formula, then $\lnot !A$ source is a formula.
If $!A$ source and $!B$ source are formulas, then $(!A \land !B)$ source is a formula.
If $!A$ source and $!B$ source are formulas, then $(!A \lor !B)$ source is a formula.
If $!A$ source and $!B$ source are formulas, then $(!A \lif !B)$ source is a formula.
If $!A$ source is a formula, then $\Ptemp !A$ source, $\Htemp !A$ source, $F !A$ source, $\Gtemp !A$ source are all formulas.
Nothing else is a formula.

The semantics of temporal logics are given in terms of relational models, as with other kinds of intensional logics.

Definition of a temporal model

A model for temporal language is a triple $\mModel{M} = \tuple{T, \prec, V}$ source, where

$T$ source is a nonempty set, interpreted as points in time.
$\prec$ source is a binary relation on $T$ source.
$V$ source is a function assigning to each propositional variable $p$ source a set $V(p)$ source of points in time.

When $t \prec t'$ source holds, we say that $t$ source precedes $t'$ source. When $t \in V(p)$ source we say $p$ source is true at $t$ source.

For now, you will notice that we do not impose any conditions on our precedence relation $\prec$ source. This means that at present, there are no restrictions on the structure of our temporal models, so we could have models in which time is linear, branching, circular, or has any structure whatsoever.

Just as with normal modal logic, every temporal model determines which formulas count as true at which points in it. We use the same notation “model $\mModel{M}$ source makes formula $!A$ source true at point $t$ source” for the basic notion of relational semantics. The relation is defined inductively and is identical to the normal modal case for all non-modal operators.

Definition of truth in a temporal model

Truth of a formula $!A$ source at $t$ source in a $\mModel M$ source, in symbols: $\mSat{M}{!A}[t]$ source, is defined inductively as follows:

Case: $!A \ident \lfalse$ source
Never $\mSat{M}{\lfalse}[t]$ source.
$\mSat{M}{p}[t]$ source iff $t \in V(p)$ source
Case: $!A \ident \lnot !B$ source
$\mSat{M}{\indfrm}[t]$ source iff $\mSat/{M}{!B}[t]$ source.
Case: $!A \ident (!B \land !C)$ source
$\mSat{M}{\indfrm}[t]$ source iff $\mSat{M}{!B}[t]$ source and $\mSat{M}{!C}[t]$ source.
Case: $!A \ident (!B \lor !C)$ source
$\mSat{M}{\indfrm}[t]$ source iff $\mSat{M}{!B}[t]$ source or $\mSat{M}{!C}[t]$ source (or both).
Case: $!A \ident (!B \lif !C)$ source
$\mSat{M}{\indfrm}[t]$ source iff $\mSat/{M}{!B}[t]$ source or $\mSat{M}{!C}[t]$ source.
Case: $!A \ident \Ptemp !B$ source
$\mSat{M}{\indfrm}[t]$ source iff $\mSat{M}{!B}[t']$ source for some $t' \in T$ source with $t' \prec t$ source
Case: $!A \ident \Htemp !B$ source
$\mSat{M}{\indfrm}[t]$ source iff $\mSat{M}{!B}[t']$ source for every $t' \in T$ source with $t' \prec t$ source
Case: $!A \ident \Ftemp !B$ source
$\mSat{M}{\indfrm}[t]$ source iff $\mSat{M}{!B}[t']$ source for some $t' \in T$ source with $t \prec t'$ source
Case: $!A \ident \Gtemp !B$ source
$\mSat{M}{\indfrm}[t]$ source iff $\mSat{M}{!B}[t']$ source for every $t' \in T$ source with $t \prec t'$ source

Based on the semantics, you might be able to see that the operators $\Ptemp$ source and $\Htemp$ source are duals, as well as the operators $\Ftemp$ source and $\Gtemp$ source, such that we could define $\Htemp !A$ source as $\lnot \Ptemp \lnot !A$ source, and the same with $\Gtemp$ source and $\Ftemp$ source.

Properties of Temporal Frames

Given that our temporal models do not impose any conditions on the relation $\prec$ source, the only one of our familiar axioms that holds in all models is $K$ source, or its analogues $K_{\Gtemp}$ source and $K_{\Htemp}$ source:

\tag{$K_{\Gtemp}$} \Gtemp (p \to q) & \to (\Gtemp p \to \Gtemp q)\\ \tag{$K_{\Htemp}$} \Htemp (p \to q) & \to (\Htemp p \to \Htemp q)

source

However, if we want our models to impose stricter conditions on how time is represented, for instance by ensuring that $\prec$ source is a linear order, then we will end up with other validities in our models.

Temporal frame correspondence table

[t]

Five temporal frame correspondence rows

Temporal frame correspondence table. Column headers: if the precedes relation has the stated property; then the displayed formula is true in model M. Row one, transitive: for every u, v, and w, if u precedes v and v precedes w, then u precedes w; corresponding formula if it will sometime be the case that p will sometime be the case, then p will sometime be the case. Row two, linear: for every w and v, either w precedes v, w equals v, or v precedes w; corresponding formula if either it will sometime be the case that p was once the case, or it was once the case that p will sometime be the case, then either p was once the case, p is now the case, or p will sometime be the case. Row three, dense: for every w and v, if w precedes v, then there is a u such that w precedes u and u precedes v; corresponding formula if p will sometime be the case, then it will sometime be the case that p will sometime be the case. Row four, unbounded toward the past: for every w there is a v that precedes w; corresponding formula if p has always been the case, then p was once the case. Row five, unbounded toward the future: for every w there is a v such that w precedes v; corresponding formula if p will always be the case, then p will sometime be the case. End table.

Five temporal frame correspondence rows
If $\prec$ source has the stated property	Then this formula is true in $\mModel{M}$ source
$\forall u \forall v \forall w ((u \prec v \land v \prec w) \lif u \prec w)$ source	$\Ftemp \Ftemp p \lif \Ftemp p$ source
$\forall w \forall v (w \prec v \lor w = v \lor v \prec w)$ source	$(\Ftemp \Ptemp p \lor \Ptemp \Ftemp p) \lif (\Ptemp p \lor p \lor \Ftemp p)$ source
$\forall w \forall v (w \prec v \to \exists u(w \prec u \land u \prec v))$ source	$\Ftemp p \lif \Ftemp \Ftemp p$ source
$\forall w \exists v( v \prec w)$ source	$\Htemp p \to \Ptemp p$ source
$\forall w \exists v( w \prec v)$ source	$\Gtemp p \to \Ftemp p$ source

source 26

captionSome temporal frame correspondence properties.

Several of the properties from the table of temporal frame correspondence properties might seem like desirable features for a model that is intended to represent time. However, it is worth noting that, even though we can impose whichever conditions we like on the $\prec$ source relation, not all conditions correspond to formulas that can be expressed in the language of temporal logic. For example, irreflexivity, or the idea that $\forall w \lnot (w \prec w)$ source, does not have a corresponding formula in temporal logic.

Additional Operators for Temporal Logic

In addition to the unary operators for past and future, temporal logics also sometimes include binary operators $\Since$ source and $\Until$ source, intended to symbolize “since” and “until”. This means adding $\Since$ source and $\Until$ source into the language of temporal logic and adding the following clause into the definition of a temporal formula:

If $!A$ source and $!B$ source are formulas, then $(\Since !A !B)$ source and $(\Until !A !B)$ source are both formulas.

The semantics for these operators are then given as follows:

Truth conditions for since and until

Truth of a formula $!A$ source at $t$ source in a $\mModel M$ source:

Case: $!A \ident \Since !B !C$ source
$\mSat{M}{\indfrm}[t]$ source iff $\mSat{M}{!B}[t']$ source for some $t' \in T$ source with $t' \prec t$ source, and for all $s$ source with $t' \prec s \prec t$ source, $\mSat{M}{!C}[s]$ source
Case: $!A \ident \Until !B !C$ source
$\mSat{M}{\indfrm}[t]$ source iff $\mSat{M}{!B}[t']$ source for some $t' \in T$ source with $t \prec t'$ source, and for all $s$ source with $t \prec s \prec t'$ source, $\mSat{M}{!C}[s]$ source

The intuitive reading of $\Since !B !C$ source is “Since $!B$ source was the case, $!C$ source has been the case.” And the intuitive reading of $\Until !B !C$ source is “Until $!B$ source will be the case, $!C$ source will be the case.”

Possible Histories

The relational models of temporal logic that we have been using are extremely flexible, since we do not have to place any restrictions on the accessibility relation. This means that temporal models can branch in the past and in the future, but we might want to consider a more “modal” conception of branching, in which we consider sequences of events as possible histories. This does not necessarily require changing our language, though we might also add our “ordinary” modal operators $\Box$ source and $\Diamond$ source, and we could also consider adding epistemic accessibility relations to represent changes in agents' knowledge over time.

Definition of a possible-histories model

A possible histories model for the temporal language is a triple $\mModel{M} = \tuple{T, C, V}$ source, where

$T$ source is a nonempty set, interpreted as states in time.
$C$ source is a set of computational paths, or possible histories of a system. In other words, $C$ source is a set of sequences $\sigma$ source of states $s_1$ source, $s_2$ source, $s_3$ source, dots, where every $s_i \in T$ source.
$V$ source is a function assigning to each propositional variable $p$ source a set $V(p)$ source of points in time.

To make things simpler, we will also generally assume that when a history is in $C$ source, then so are all of its suffixes. For example, if $s_1$ source, $s_2$ source, $s_3$ source is a sequence in $C$ source, then so are $s_2$ source, $s_3$ source and $s_3$ source. Also, when two states $s_i$ source and $s_j$ source appear in a sequence $\sigma$ source, we say that $s_i \prec_\sigma s_j$ source when $i < j$ source. When $t \in V(p)$ source we say $p$ source is true at $t$ source.

The one relevant change is that when we evaluate the truth of a formula at a point in time $t$ source in a model $\mModel M$ source, we do so relative to a history $\sigma$ source, in which $t$ source appears as a state. We do not need to change any of the semantics for propositional variables or for truth-functional connectives, though. All of those are exactly as they were in the definition of truth at a point in a temporal model, since none of those will make reference to $\sigma$ source. However, we now redefine our future operator $\Ftemp$ source and add our $\Diamond$ source operator with respect to these histories.

Truth relative to a possible history

Truth of a formula $!A$ source at $t, \sigma$ source in $\mModel M$ source, in symbols: $\mSat{M}{!A}[t, \sigma]$ source:

Case: $!A \ident \Ftemp !B$ source
$\mSat{M}{\indfrm}[t, \sigma]$ source iff $\mSat{M}{!B}[t', \sigma]$ source for some $t' \in T$ source such that $t \prec_\sigma t'$ source.
Case: $!A \ident \Diamond !B$ source
$\mSat{M}{\indfrm}[t, \sigma]$ source iff $\mSat{M}{!B}[t, \sigma']$ source for some $\sigma' \in C$ source in which $t$ source occurs.

Other temporal and modal operators can be defined similarly. However, we can now represent claims that combine tense and modality. For example, we might symbolize “ $p$ source will not occur, but it might have occurred” using the formula $\lnot \Ftemp p \land \Diamond \Ftemp p$ source. This would hold at a point and a history at which $p$ source does not become true at a successor state, but there is an alternative history at which $p$ source will become true.

Source disclosures

TR057-SAR-001: Source typography note. The phrase denumerable set carries a plural suffix after the glossary term, yielding denumerables set. The wording is preserved without changing the immutable source. source
TR057-SAR-002: Source notation note. The future-sometime formula in this induction clause is printed as the plain letter F followed by A, unlike the future-operator macro used elsewhere. It is spoken as the source's plain letter F and is not silently replaced. source