Temporal Logic
What?
A temporal logic is a logistic system that allows you to describe and reason about when statements are true.
Why?
Architects and designers can employ temporal logic as a very useful way to formalize statements about a system and prove them correct.
Systems of Temporal Logic
There are many systems of temporal logic; most are based on Prior’s tense logic (and enhancements). A particularly useful kind of temporal logic for computer scientists is one in which time is viewed as discrete (rather than continuous), considers branching time (as opposed to linear time) and in which time branches only into the future (and not into the past).
In such a system the operators include all the basic operators from predicate calculus:
- $T$ meaning true
- $F$ meaning false
- $\neg p$ meaning not $p$
- $p \wedge q$ meaning $p$ is true and $q$ is true
- $p \vee q$ meaning $p$ is true or $q$ is true
- $p \supset q$ meaning $p$ materially implies $q$
- $\forall x.\,p$ meaning $p$ is true for every $x$
- $\exists x.\,p$ meaning $p$ is true for some $x$
as well as:
- $\Box p$ meaning $p$ is true from now on
- $\lozenge p$ meaning $p$ will eventually be true
- $\mathbf{O}\,p$ meaning $p$ is true at the next time instant
- $p\,\mathbf{U}\,q$ meaning $p$ is true until $q$ is true
- $p\,\mathbf{S}\,q$ meaning $p$ is true since $q$ is true
- $\mathbf{A}\,p$ meaning $p$ is true in all possible futures (A = always)
- $\mathbf{E}\,p$ meaning $p$ is true in some possible future (E = eventually)
Fancier systems of temporal logic include operators such as
- $\overline{\Box}\,p$ meaning $p$ is true always in the past
- $\overline{\lozenge}\,p$ meaning $p$ is true sometimes in the past
- $\overline{\mathbf{O}}\,p$ meaning $p$ was true at the previous time instant
- $p\,\mathbf{W}\,q$ meaning $p$ waiting for $q$
- $p\,\mathbf{B}\,q$ meaning $p$ back-to $q$
Leslie Lamport’s TLA (Temporal Logic of Actions) is a well-developed system useful for “specifying and reasoning about concurrent and reactive systems.”