THE TEMPORAL LOGIC

A logic that speaks of the future: always, eventually, until. Linear temporal logic reads a formula against a path through time — not one state, but the whole unfolding — and decides what a system does forever, not just once. Rendered, not quoted.

source Amir Pnueli, The Temporal Logic of Programs, 18th FOCS, IEEE (1977), pp. 46–57 — doi:10.1109/SFCS.1977.32 (proceedings paywalled — DOI stable)

Blue Team · builds & defends
3

The Model

A path is an infinite sequence of states. We give it finitely as a lasso: a prefix then a loop that repeats forever. Each state fixes which atoms hold.

Atoms here: p, q. States s0 s1 s2, loop back from s2→s1. Position i maps to a real state by unfolding the loop, so the future from any i is well-defined.

op(φ,i): X φ = φ at i+1 F φ = φ at some j≥i G φ = φ at all j≥i p U q = q at some j≥i, p at all k in [i,j)
5

The Lineage

Logic about time. Pnueli lifted tense logic onto program runs so a proof could say “this holds forever” or “this eventually happens.”

These same operators are the language that the-model-checking decides — a checker takes an LTL formula and a system and answers whether every run satisfies it. Here we evaluate on one path; a model checker quantifies over all of them.

7

The Witness

A live re-check of the operator semantics against an independent reference (reachable-state scan). Green while the engine matches the definitions; it flips red the instant the tamper (6) corrupts F.

…
The Machine
4

Data In in ↓

The lasso path and a formula to evaluate.

loop ↻ s1 → s2 → s1 … (repeats forever)
↓ evaluate ↓
0

The Panel LIT

Pick a formula — evaluated live at position 0 over the infinite unfolding.

↓ proven ↓
8

Data Out out ↓

G p = false   F q = true   p U q = true

All operator laws (duality, expansion, until) verified exhaustively over the lasso.

…
Red Team · attacks & breaks
1

The Adversary WALL

“Eventually just means it happens somewhere, so I only need to look at the state I’m in.” No. F p ranges over the whole future. On a lasso that future is infinite; a naive checker that stops at the current state, or that never enters the loop, reports liveness properties wrong. The horizon must cover one full loop.
2

The Graveyard

  • G p = ¬F p.The dual of G is F: G p = ¬F¬p. Confusing the two swaps “always” and “never.”
  • F p = p ∨ X(F p) can stop unrolling anywhere.On a lasso you must unroll at least one full period, or a p that only appears in the loop is missed.
  • p U q holds if q ever holds later.Until also demands p at every step strictly before that q. Drop it and you accept paths that violated p first. AMBER: this is strong (non-weak) until — q is required to occur.
6

The Tamper

Planted void (disclosed): evaluate F φ as “φ holds at position 0” instead of “at some position.” A formula that only becomes true later is then wrongly reported false. Witness (7) catches it live.