Temporal Logic: LTL and CTL

Propositional logic can say what is true now — "the light is green", "the buffer is full". But a reactive system lives in time: what we really want to promise is that a request will eventually be answered, that the alarm stays raised until it is acknowledged, that the system can always get back to a safe state. Ordinary logic has no words for "eventually", "always", "until", "next". Temporal logic supplies exactly those words — modal operators over time — and turns the vague english of a safety or liveness requirement into a formula a machine can check.

There are two great dialects, and the difference between them is a difference in how they see time itself. LTL (Linear Temporal Logic) sees each run as a single line stretching into the future. CTL (Computation Tree Logic) sees the future as a branching tree of possibilities and lets you quantify over the branches. Learning both — and learning where they genuinely disagree — is the heart of specifying behaviour over time.

LTL: reasoning along a single path

LTL formulas are evaluated over one infinite trace \pi = s_0\, s_1\, s_2 \ldots On top of the ordinary connectives (\neg, \wedge, \vee, \rightarrow) it adds four temporal operators that talk about the suffix of the path from the current position onward.

\mathbf{X}\,\varphi — neXt: \varphi holds at the next state, s_1.
\mathbf{F}\,\varphi — Finally / eventually: \varphi holds at some state s_i, i \ge 0.
\mathbf{G}\,\varphi — Globally / always: \varphi holds at every state on the path.
\varphi\, \mathbf{U}\, \psi — Until: \psi eventually holds, and \varphi holds at every state until it does.

Two identities are worth burning in: \mathbf{F}\,\varphi \equiv \texttt{true}\,\mathbf{U}\,\varphi (eventually is "until, with no side-condition") and the duality \mathbf{G}\,\varphi \equiv \neg\mathbf{F}\,\neg\varphi ("always \varphi" is "never not-\varphi"), the temporal echo of \forall = \neg\exists\neg. A formula holds for the system when it holds for every path the system can take.

Reading real specifications

The power of LTL is that ordinary engineering wishes translate almost word-for-word. Nesting \mathbf{G} and \mathbf{F} gives the two workhorse patterns.

LTL formula	In words	Property class
\mathbf{G}\,\neg(cs_1 \wedge cs_2)	the two critical sections are never occupied at once	safety
\mathbf{G}(req \rightarrow \mathbf{F}\,ack)	every request is eventually acknowledged (request–response)	liveness
\mathbf{G}\,\mathbf{F}\,enabled	the process is enabled infinitely often (a fairness assumption)	liveness
\mathbf{F}\,\mathbf{G}\,stable	eventually the system settles and stays stable forever	liveness
alarm\,\mathbf{U}\,reset	the alarm stays on until (and a reset does occur) it is reset	—

The star is \mathbf{G}(req \rightarrow \mathbf{F}\,ack): "at every moment, if a request is seen, then an acknowledgement eventually follows." That one pattern captures the correctness of an astonishing range of protocols, servers and controllers. And \mathbf{G}\,\mathbf{F}\,p ("infinitely often p") versus \mathbf{F}\,\mathbf{G}\,p ("eventually always p") is the classic subtle pair — the first allows p to keep flickering off, the second demands it eventually latch on for good.

CTL: reasoning over the branching tree

LTL says nothing about "could" versus "must": it only ever asserts things about the paths, all of them. But sometimes you want "from every reachable state there exists a way back to a safe state" — a statement about the branching of the future, not any single line. CTL sees the unrolling of the system as a computation tree: the current state at the root, and a branch for every possible next step, forever. The figure shows the first few levels.

CTL pairs a path quantifier with a temporal operator, and the two must come together:

Path quantifiers. \mathbf{A} — "for All paths from here"; \mathbf{E} — "there Exists a path from here".
Combine each with \mathbf{X}, \mathbf{F}, \mathbf{G}, \mathbf{U} to get eight modalities: \mathbf{AX}, \mathbf{EX}, \mathbf{AF}, \mathbf{EF}, \mathbf{AG}, \mathbf{EG}, \mathbf{A}[\cdot\mathbf{U}\cdot], \mathbf{E}[\cdot\mathbf{U}\cdot].
Read them: \mathbf{AG}\,\varphi = "\varphi on all states of all paths — an invariant"; \mathbf{EF}\,\varphi = "some path reaches a \varphi-state — \varphi is reachable"; \mathbf{AF}\,\varphi = "every path eventually hits \varphi — inevitability".

The showcase CTL specification is \mathbf{AG}\,\mathbf{EF}\,safe: "on every reachable state (\mathbf{AG}), there exists a path back to a safe state (\mathbf{EF}\,safe)." This "you can always recover" property — no reachable state is a trap — cannot be expressed in LTL at all, because LTL has no way to say "there exists a continuation."

Linear vs branching: two lenses on time

LTL and CTL are genuinely incomparable — each can express things the other cannot, so neither subsumes the other.

Only CTL: \mathbf{AG}\,\mathbf{EF}\,restart — "from everywhere it is possible to reach a restart." The nested \mathbf{E} quantifies over branches; LTL, which speaks only of "all paths", cannot say "some path exists."
Only LTL: \mathbf{F}\,\mathbf{G}\,p — "on every run, eventually p holds forever." The naive CTL translation \mathbf{AF}\,\mathbf{AG}\,p is strictly stronger and not equivalent — there are systems satisfying the LTL formula but not the CTL one.
The shared core is called CTL* — a logic that freely mixes path quantifiers and temporal operators and contains both LTL and CTL as fragments.

Which lens to use is partly taste, partly tooling. LTL's "reason about one path at a time" matches how we describe runs and traces, and its counterexamples are single executions; CTL's branching view expresses "possibility" properties and, as you will see, admits a beautifully simple model-checking algorithm that runs in time linear in the formula and the state space.

In CTL the temporal operators are only defined relative to a set of paths, so a bare \mathbf{F}\,p at a branching state is genuinely ambiguous — eventually p on which path? CTL resolves this by syntax: every \mathbf{X}/\mathbf{F}/\mathbf{G}/\mathbf{U} must be immediately prefixed by an \mathbf{A} or an \mathbf{E}, so each temporal claim is pinned to "all continuations" or "some continuation." That is also exactly why \mathbf{F}\,\mathbf{G}\,p — two temporal operators with only one quantifier out front — is not a CTL formula: it is legal in LTL (one implicit "for all paths" wraps the whole thing) and in CTL* (which drops the pairing rule), but not in vanilla CTL.

A common trap is to "translate" an LTL formula into CTL by sprinkling \mathbf{A} in front of each operator. Take \mathbf{F}\,\mathbf{G}\,p ("on this run, eventually p stays true forever"). The mechanical CTL version \mathbf{AF}\,\mathbf{AG}\,p says "every path reaches a state from which p holds on all onward branches" — strictly stronger. A system can satisfy \mathbf{F}\,\mathbf{G}\,p on every individual path yet fail \mathbf{AF}\,\mathbf{AG}\,p, because the point at which p "latches" can differ from branch to branch, so no single state has \mathbf{AG}\,p below it. Moral: you cannot mechanically convert between the two logics — they see time differently, and the differences are real, not cosmetic.