A temporal logic is a logistic system that allows you to describe and reason about when statements are true.
Architects, designers, and analysts can employ temporal logic to reason about concurrent, dynamic systems and prove them correct.
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.
Haha, sorry, j/k.
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.
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:
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$.
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 |
TODO
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:
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
Temporal logic is a kind of modal logic and is related to dynamic logic.
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.
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:
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:
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) |
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:
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 |
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
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
We’ve covered: