Writing a temporal-logic specification is only half the battle. Now comes the question that has occupied verification for forty years: given a model of the system M and a temporal formula \varphi, does the system satisfy the specification? We write this M \models \varphi. What makes model checking revolutionary is that, for finite-state systems, this question is decidable and automatic: you hand a tool the model and the property, and it answers "yes" — or, far more usefully, hands you a concrete counterexample showing exactly how the property fails.

That last feature is the killer app. A theorem prover that says "your invariant does not follow" leaves you to guess why. A model checker that says "no" gives you a precise, replayable execution trace marching into the bug. This is push-button verification, and it earned Edmund Clarke, E. Allen Emerson, and Joseph Sifakis the 2007 Turing Award.

The model: a Kripke structure

The system is modelled as a Kripke structure (equivalently, a finite transition system): a finite set of states, a transition relation saying which state can follow which, an initial state, and — crucially — a labelling that tags each state with the atomic propositions true there. Formally M = (S, S_0, R, L) with R \subseteq S \times S total (every state has a successor, so runs are infinite) and L : S \to 2^{AP}.

The paths through this graph are the behaviours: unrolling the Kripke structure from the initial state gives exactly the computation tree the temporal logic talks about. So M \models \varphi means "every path (or, for CTL, the branching structure) from S_0 satisfies \varphi" — a question about a finite graph, which is why it can be decided by search.

CTL model checking: iterative fixpoint labelling

CTL has an elegant algorithm that is a joy to run by hand. Work bottom-up over the syntax tree of \varphi: for each subformula, compute the exact set of states that satisfy it, labelling states as you go. Atomic propositions are read straight off L; boolean connectives are set operations on the labels; the temporal modalities are computed by fixpoint iteration over the transition relation.

Every CTL modality reduces to \mathbf{EX}, \mathbf{EU}, \mathbf{EG} plus negation, so these three iterations decide any CTL formula. Each iteration touches every state and edge at most a bounded number of times, giving the celebrated bound: CTL model checking runs in O(|\varphi| \cdot (|S| + |R|)) — linear in both the formula and the model.

LTL model checking: the automata-theoretic product

LTL takes a different, equally beautiful route — the automata-theoretic approach of Vardi and Wolper. To check M \models \varphi, ask the complementary question: is there any run of M that violates \varphi, i.e. that satisfies \neg\varphi?

The "reachable accepting cycle" search is done by a nested depth-first search over the product graph. The whole procedure is linear in the size of the product but the automaton A_{\neg\varphi} can be exponential in |\varphi|, so LTL model checking is O\!\left(|S| \cdot 2^{O(|\varphi|)}\right) — cheap in the (usually small) formula, linear in the (usually huge) state space. Note the shapes match the previous lesson: a safety violation surfaces as a finite path to a bad state, a liveness violation as an accepting cycle.

Counterexamples: the feature that changed engineering

Why did model checking, rather than theorem proving, break into industry? Because it is refutation-oriented. When the property fails, the tool does not shrug — it produces the witness the theory guarantees: a finite trace for a safety bug, a lasso for a liveness bug, replayable step by step in the very states of your model. Engineers debug against it exactly as against a failing test, but this "test" was found by exhaustively searching all behaviours, not the handful you thought to write.

The industrial track record is why this matters. Hardware model checking is standard practice at every major chip maker — Intel adopted it in earnest after the 1994 Pentium FDIV bug. Symbolic model checkers found real errors in the cache-coherence protocols of the IEEE Futurebus+ standard and in published network and security protocols. NASA and aerospace groups model-check flight-control and mission software. The pattern is always the same: an exhaustive search over an astronomically large state space, and a short, damning counterexample when something is wrong.