THE MODEL CHECKING

Verify a property by exploring every state a system can reach. Give a machine a finite graph of states and a temporal formula, and it returns the exact set of states that satisfy it — computed by iterating a fixpoint over the transition relation, not by testing a few runs. Rendered, not quoted.

source Clarke & Emerson (1981), Design and synthesis of synchronization skeletons using branching time temporal logic, LNCS 131 · Queille & Sifakis (1982), CESAR — Springer LNCS 131 (paywalled; cited author/title/year — AMBER)

Blue Team · builds & defends
3
The Model

A finite Kripke structure K = (S, R, L): states S={0..4}, a total transition relation R, and atomic labels L. Atom p marks a goal state; bad marks an error.

R: 0→1 · 1→2 · 1→4 · 2→3 · 3→3 · 4→4. Every state has a successor (total), so EX/AX are well-defined.

CTL is evaluated over branching time: at each state the future forks along every outgoing edge.

5
The Lineage

Model checking made the-temporal-logic decidable on a finite graph. Pnueli's temporal operators say what must hold along time; Clarke & Emerson's labeling algorithm turns each operator into a fixpoint over the transition relation and computes its whole satisfying set.

That is how protocols and hardware are verified: check every path a system can take, not a sampled few. The neighbour sphere supplies the logic; this one supplies the decision procedure.

7
The Witness · live re-check

Re-runs the labeling algorithm on the live structure and compares EF p against the canonical set proved at boot. Flips red the instant the transition relation is tampered.

witness idle

Canonical EF p (sealed at boot):

The Machine
4
in ↓ Data In

The structure K above, plus three CTL properties to decide:

EF p  ·  AG p  ·  AG(¬bad)

EF p = "a p-state is reachable" (some path eventually p). AG p = "p holds on all reachable states" (every path always p). AG(¬bad) = a safety property.

▼ ▼ ▼
0
LIT The Panel · live engine

Labeling / fixpoint algorithm. EX(Z)=states with a successor in Z; AX(Z)=states with all successors in Z.

EF p = μZ. p ∨ EX Z → (least fixpoint)
AG p = νZ. p ∧ AX Z → (greatest fixpoint)
AG(¬bad) → safety set

▼ ▼ ▼
8
out ↓ Data Out

Every set below equals the CTL semantic definition, verified by exhaustive set-equality (fixpoint vs. independent BFS reachability).

booting…
Red Team · attacks & breaks
1
WALL The Adversary
"Just simulate a few runs and if none hit bad, it's safe." — Testing samples paths; it can only ever find bugs, never prove their absence. Model checking is exhaustive precisely because a missed path is a missed counterexample.
"Fixpoints are optional — one step of EX is enough for reachability." False: a p-state reached in two or more hops is invisible after one step. Reachability is the transitive closure of EX. (Window 6 weaponises exactly this.)

Real limit: state explosion — |S| is exponential in the number of variables. The set-equality here is honest only because |S|=5.

2
The Graveyard
"EF p and AG p are duals, so AG p = ¬EF p."
✔ AG p = ¬EF(¬p), not ¬EF(p). Here ¬EF(p)={4} but AG p={3}. The negation goes inside.
"If no bad state carries a self-loop, AG(¬bad) holds."
✔ Safety depends on reachability of bad, not its loops. bad=4 is reachable via 0→1→4, so AG(¬bad) fails at state 0.
"The greatest fixpoint starts from ∅."
✔ ν starts from all states and shrinks; μ starts from the target and grows. Swapping them inverts the answer.
6
The Tamper · planted void

Disclosed sabotage: replace the EF fixpoint with a single EX step. States that reach p in 2+ hops (0 and 1) are dropped.

The Witness (7) recomputes live and catches the mismatch every time.