Temporal Logic

Time may be an illusion, but that doesn’t mean we can’t reason about it.

What?

A temporal logic is a logistic system that allows you to describe and reason about when statements are true.

Why?

Architects, designers, and analysts can employ temporal logic to reason about concurrent, dynamic systems and prove them correct.

Who?

Big names in Temporal Logic include: Arthur Prior, who invented tense logic; Leslie Lamport, who developed TLA (Temporal Logic of Actions); and E. Allen Emerson, who worked on model checking and temporal logic.

Another “who” is the Stanford Encyclopedia of Philosophy, whose articles on Temporal Logic and Modal Logic are fantastic.

Exercise: After browsing the notes on page you are reading now, read the full article on Temporal Logic in the Stanford Encyclopedia of Philosophy. What are some of the key differences between temporal logic and other modal logics? How does temporal logic relate to the general concept of time in philosophy?

When?

Haha, sorry, j/k.

Which

There are many systems of temporal logic; most are based on Prior’s tense logic (and enhancements). They vary on such aspects as:

Whether time is discrete or continuous
Whether it is branching or linear
If branching, whether it branches only into the past or only the future or both
Whether the future is bounded or unbounded
Whether the primitive units of time are instants or intervals
Whether explicit time bounds or durations are included (i.e., “real-time”)
What choices are made for the axioms

In computing, we generally take time to be discrete and branching into the future only. But, hey, if something better works for you, go for it. Don’t allow your thinking to be limited.

Notation

Usually, a temporal logic starts with the basic operators from predicate calculus:

Operator	Meaning
$T$	true
$F$	false
$\neg \varphi$	not $\varphi$
$\varphi \wedge \psi$	$\varphi$ is true and $\psi$ is true
$\varphi \vee \psi$	$\varphi$ is true or $\psi$ is true
$\varphi \supset \psi$	$\varphi$ materially implies $\psi$
$\forall x.\,\varphi$	$\varphi$ is true for every $x$
$\exists x.\,\varphi$	$\varphi$ is true for some $x$

as well as:

Operator	Meaning
$\mathbf{G}\,\varphi \quad or\quad \Box \varphi$	$\varphi$ is always GOING to be true
$\mathbf{F}\,\varphi \quad or\quad \lozenge \varphi$	$\varphi$ is (eventually) true at some FUTURE point
$\mathbf{H}\,\varphi \quad or\quad \overline{\Box}\,\varphi$	$\varphi$ always HAS been true
$\mathbf{P}\,\varphi \quad or\quad \overline{\lozenge}\,\varphi$	$\varphi$ was true at some point in the PAST
$\mathbf{O}\,\varphi \quad or\quad \bigcirc \varphi$	$\varphi$ is true at the next time instant
$\overline{\mathbf{O}}\,\varphi \quad or\quad \overline{\bigcirc}\,\varphi$	$\varphi$ was true at the previous time instant
$\varphi\,\mathbf{U}\,\psi$	$\varphi$ is true until $\psi$ is true
$\varphi\,\mathbf{S}\,\psi$	$\varphi$ is true since $\psi$ is true
$\varphi\,\mathbf{W}\,\psi$	$\varphi$ is waiting for $\psi$ to be true
$\varphi\,\mathbf{B}\,\psi$	$\varphi$ back-to $\psi$

Although you will commonly see $\Box$ and $\lozenge$ used for temporal modalities, it’s probably better to stick with Arthur Prior’s original tense operators ($\mathbf{P}$, $\mathbf{H}$, $\mathbf{F}$, and $\mathbf{G}$). This is because $\Box$ and $\lozenge$ are traditionally defined to be the alethic modalities “necessarily” and “possibly.” This way you can distinguish:

$\Box\mathbf{F}c$ for I will cook dinner, i.e., it is necessary that in the future, I will cook dinner
$\lozenge\mathbf{F}c$ for I might cook dinner, i.e., it is possible that in the future, I will cook dinner

If you steal $\Box$ and $\lozenge$ for temporal modalities, you’ll have to invent new operators to get back the necessary and the possible. People have done this hack:

Operator	Meaning
$\mathbf{A}\,\varphi$	$\varphi$ is true in all possible futures
$\mathbf{E}\,\varphi$	$\varphi$ is true in some possible future

Then you can say $\mathbf{A}c$ and $\mathbf{E}c$.

Duality

In classical logic, operators are often duals of each other with respect to negation. You’ve probably seen that with these operators:

Dual Pair	Explanations
$\neg (\varphi \wedge \psi) \equiv (\neg \varphi \vee \neg \psi)$	It’s not the case that $\varphi$ and $\psi$ are both true $\equiv$ At least one of $\varphi$ or $\psi$ must be false
$\neg (\varphi \vee \psi) \equiv (\neg \varphi \wedge \neg \psi)$	It’s not the case that at least one of $\varphi$ and $\psi$ are true $\equiv$ $\varphi$ must be false and $\psi$ must be false
$\neg \forall x. \varphi \equiv \exists x. \neg \varphi$	Not for every $x$, $\varphi$ $\equiv$ There's an $x$ that makes $\varphi$ false
$\neg \exists x. \varphi \equiv \forall x. \neg \varphi$	There's no $x$ that makes $\varphi$ true $\equiv$ For every $x$, $\varphi$ is false
$\neg \Box \varphi \equiv \lozenge \neg \varphi$	It’s not the case that $\varphi$ is necessarily true $\equiv$ It's possible that $\varphi$ is false
$\neg \lozenge \varphi \equiv \Box \neg \varphi$	It’s not the case that $\varphi$ is possibly true $\equiv$ It's necessary that $\varphi$ is false

In temporal logic, we have similar dualities, $\mathbf{P}$ and $\mathbf{H}$ are duals of each other, and $\mathbf{F}$ and $\mathbf{G}$ are duals:

Dual Pair	Explanations
$\neg \mathbf{G}\, \varphi \equiv \mathbf{F}\, \neg \varphi$	It’s not the case that $\varphi$ will always be true from now on $\equiv$ At some point in the future, $\varphi$ will be false
$\neg \mathbf{F}\, \varphi \equiv \mathbf{G}\, \neg \varphi$	It’s not the case that $\varphi$ will be true at some point in the future $\equiv$ $\varphi$ will always be false from now on
$\neg \mathbf{H}\, \varphi \equiv \mathbf{P}\, \neg \varphi$	It’s not the case that $\varphi$ has always been true $\equiv$ There was a point in the past at which $\varphi$ was false
$\neg \mathbf{P}\, \varphi \equiv \mathbf{H}\, \neg \varphi$	It’s not the case that $\varphi$ was true at some point in the past $\equiv$ $\varphi$ has always been false

Examples

TODO

Systems of Temporal Logic

Perhaps it all started with Arthur Prior’s basic tense logic TL, with the four operators $\mathbf{P}$, $\mathbf{H}$, $\mathbf{F}$, and $\mathbf{G}$. They were okay at specifying some tenses but there were some things they could not capture. Extensions soon followed, and today these can be broadly categorized into two types:

Linear Temporal Logic (LTL): This system assumes a linear progression of time, where each moment leads to exactly one future. That is, time is a linear sequence of states, useful for describing properties of individual execution paths. Often used in computer science for specifying properties of systems.
Branching Temporal Logic (BTL): This system allows for branching time, where each moment can lead to multiple possible futures. It is useful for reasoning about systems with multiple potential outcomes. These were explored by the philosophers Charles Sanders Peirce (see Peircean Temporal Logic) and William of Ockham (see Ockhamist Temporal Logic)

Some specific systems include:

CTL (Computation Tree Logic): A branching time logic that allows for quantification over paths, allowing reasoning about multiple possible futures.
CTL*: An extension of CTL that combines both linear and branching time features.
ATL (Alternating-time Temporal Logic): Used for reasoning about multi-agent systems and their strategies.
ITL (Interval Temporal Logic): Uses intervals as the basic entities, allowing for reasoning about durations and relationships between events occurring within those intervals.

For details, check out the Wikipedia articles in the order below:

TLA⁺

Leslie Lamport’s TLA (Temporal Logic of Actions) is a well-developed system useful for “specifying and reasoning about concurrent and reactive systems.”

This one is very useful in CS so it gets its own section.

TODO

Related Types of Logic

Temporal logic is a kind of modal logic and is related to dynamic logic.

Modal Logics

Temporal logic is a modal logic, meaning it deals with modalities, or ways of qualifying truth. In the case of temporal logic, the modalities relate to time (in the future, in the past, at the next instant, and so on). But there are quite a few other kinds of modalities, giving rise to different logics.

Exercise: Read about Modal Logic in the Stanford Encyclopedia of Philosophy, Wikipedia, and at nLab. Are there any kinds of modal logics mentioned there that are not mentioned below?

Alethic Logic (Necessity and Possibility)

Form	Meaning
$\Box\,\varphi$	It is necessary that $\varphi$ is true
$\lozenge\,\varphi$	It is possible that $\varphi$ is true

In classical modal logic, the two operators are duals, as we saw above. Also, you can read:

$\neg \lozenge\,\varphi$ as “$\varphi$ is impossible”
$\neg \Box\,\varphi$ as “$\varphi$ is contingent”

Deontic Logic (Obligation and Permission)

Form	Meaning
$\mathscr{O}\,\varphi$	It is obligatory that $\varphi$, or $\varphi$ ought to be, or MUST be done
$\mathscr{P}\,\varphi$	It is permissible that $\varphi$, or $\varphi$ is allowed, or MAY be done

In classical deontic logic, these are duals: not obligatory means it’s permissible to not do something, and not permissible means it’s obligatory to not do something. Also, you can read:

$\neg \mathscr{P}\,\varphi$, or equivalently $\mathscr{O}\neg\varphi$ as “$\varphi$ is forbidden” (impermissible, or not permitted)

Exercise: Which of the following do you think should be valid in deontic logic: (a) From $\mathscr{O}\,\varphi$ infer $\mathscr{P}\,\varphi$, (b) From $\mathscr{O}\,\varphi$ infer $\varphi$, (c) $\mathscr{O}(\mathscr{O}\,\varphi \supset \varphi)$.

Epistemic Logic (Knowledge)

Form	Meaning
$\mathscr{K}_x \varphi$	Agent $x$ knows that $\varphi$ is true
$\mathscr{K} \varphi$	It is known that $\varphi$ is true (by all agents or by some agent whose identity we assume from context)

Doxastic Logic (Belief)

Form	Meaning
$\mathscr{B}_x\,\varphi$	Agent $x$ believes that $\varphi$ is true
$\mathscr{B}\,\varphi$	It is believed that $\varphi$ is true (by all agents or by some agent whose identity we assume from context)

The epistemic and the doxastic are often distinguished in the following context.

Let $\Gamma = \exists g. G g$, i.e., there exists a $g$ such that $g$ is a god, or “(at least one) god exists.” Then:

$\mathscr{K}_x\,\Gamma \wedge \mathscr{B}_x\,\Gamma$ means $x$ is a gnostic theist
$\mathscr{K}_x\,\Gamma \wedge \neg \mathscr{B}_x\,\Gamma$ means $x$ is a gnostic atheist
$\neg \mathscr{K}_x\,\Gamma \wedge \mathscr{B}_x\,\Gamma$ means $x$ is an agnostic theist
$\neg \mathscr{K}_x\,\Gamma \wedge \neg \mathscr{B}_x\,\Gamma$ means $x$ is a agnostic atheist

Exercise: What is the difference between $\neg \mathscr{B}_x\,\Gamma$ and $\mathscr{B}_x\,\neg \Gamma$. Explain what each is saying in English. Would most English speakers be able to tell the difference? Is one statement ”stronger” than the other?

Dynamic Logic

Dynamic Logic brings events into the picture:

Form	Meaning
$[e]\varphi$	After event $e$, $\varphi$ is necessarily true
$\langle e \rangle \varphi$	After event $e$, $\varphi$ is possibly true

Exercise: In what sense to the formulas above equate with events “causing” things to be true or not?

Temporal logic [is] the modal logic of choice for reasoning about concurrent systems with its aspects of synchronization, interference, independence, deadlock, livelock, fairness, etc. These concerns of concurrency would appear to be less central to linguistics, philosophy, and artificial intelligence, the areas in which dynamic logic is most often encountered nowadays.— Wikipedia

Recall Practice

Here are some questions useful for your spaced repetition learning. Many of the answers are not found on this page. Some will have popped up in lecture. Others will require you to do your own research.

Recall questions coming soon

Summary

We’ve covered: