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:

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:

OperatorMeaning
$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:

OperatorMeaning
$\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:

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:

OperatorMeaning
$\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 PairExplanations
$\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 PairExplanations
$\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:

Some specific systems include:

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)

FormMeaning
$\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:

Deontic Logic (Obligation and Permission)

FormMeaning
$\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:

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)

FormMeaning
$\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)

FormMeaning
$\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:

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:

FormMeaning
$[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:

  • ...