Model Checking

Overview

Model checking is an automated verification technique that exhaustively explores the state space of a finite-state system to determine whether a given property holds. If the property is violated, the model checker produces a counterexample -- a concrete execution trace demonstrating the violation.

State Space Exploration

A system is modeled as a Kripke structure M = (S, S0, R, L):

S: finite set of states
S0 ⊆ S: initial states
R ⊆ S × S: transition relation (must be total)
L : S → 2^AP: labeling function mapping states to sets of atomic propositions

Model checking asks: does M ⊨ φ (does model M satisfy property φ)?

Explicit-state exploration enumerates states one by one (BFS or DFS). Works well for asynchronous systems with moderate state spaces. Main challenge: state explosion -- the state space grows exponentially with the number of components.

Temporal Logics

LTL, CTL, and CTL* Temporal Logics

Temporal logics express properties about how system behavior evolves over time.

LTL (Linear Temporal Logic)

LTL reasons over linear paths (sequences of states). Formulas are evaluated over infinite execution traces.

Operators: | Operator | Meaning | Example | |----------|---------|---------| | X φ | Next: φ holds in the next state | X ready | | F φ | Finally: φ holds eventually | F terminated | | G φ | Globally: φ holds forever | G ¬error | | φ U ψ | Until: φ holds until ψ becomes true | waiting U granted | | φ R ψ | Release: dual of Until | φ R ψ ≡ ¬(¬φ U ¬ψ) |

Common patterns:

Safety: G ¬bad (bad thing never happens)
Liveness: G(request → F grant) (every request is eventually granted)
Fairness: GF enabled → GF executed (if infinitely often enabled, infinitely often executed)

LTL model checking works by converting ¬φ to a Buchi automaton, composing with the system, and checking for emptiness of the product automaton.

CTL (Computation Tree Logic)

CTL reasons over branching computation trees. Path quantifiers (A = all paths, E = exists a path) must immediately precede temporal operators.

Operators: AX, EX, AF, EF, AG, EG, AU, EU

AG ¬deadlock           -- no deadlock on any path (safety)
AG(request → AF grant) -- every request is granted on all paths
EF goal                -- there exists a path reaching goal
AG EF restart          -- from any state, restart is reachable

CTL model checking uses fixpoint computation on the state set:

EF φ = μZ. φ ∨ EX Z (least fixpoint)
EG φ = νZ. φ ∧ EX Z (greatest fixpoint)

CTL*

CTL* subsumes both LTL and CTL. Path quantifiers and temporal operators can be freely mixed. Example: A(FG p) (on all paths, p eventually holds forever) -- expressible in CTL* but not in CTL. Model checking CTL* is PSPACE-complete (vs PSPACE for LTL, P for CTL).

Expressiveness Comparison

        CTL*
       /    \
     LTL    CTL
       \    /
       common

F G p is in LTL but not CTL
AG EF p is in CTL but not LTL
Neither LTL nor CTL subsumes the other

Symbolic Model Checking

BDD-Based (Binary Decision Diagrams)

Represent state sets and transition relations as Ordered BDDs rather than enumerating individual states. BDDs provide a canonical, often compact representation of Boolean functions.

Transition relation R(s, s') encoded as a BDD
Image computation: given current states S, compute Post(S) = ∃s. S(s) ∧ R(s, s')
Fixpoint iterations compute reachable states or verify CTL formulas
Can handle systems with 10^20+ states (when BDDs stay compact)

Limitations: BDD variable ordering critically affects size. Some functions (e.g., multiplication) have exponential BDDs regardless of ordering.

SAT-Based / Bounded Model Checking (BMC)

Unroll the system for k steps and encode the property violation as a SAT formula:

BMC(k): I(s0) ∧ T(s0,s1) ∧ T(s1,s2) ∧ ... ∧ T(s_{k-1},s_k) ∧ ¬φ(s0,...,s_k)

If the formula is satisfiable, the satisfying assignment is a counterexample of length ≤ k.

Advantages:

Leverages powerful modern SAT/SMT solvers (CDCL, etc.)
Finds shortest counterexamples
No BDD blowup issues

Completeness: BMC alone is incomplete (cannot prove properties without a bound). Combined with k-induction or interpolation, it achieves completeness.

Major Tools

SPIN (Simple Promela Interpreter)

Models written in Promela (Process Meta Language)
Explicit-state, on-the-fly LTL model checking
Verifies safety, liveness, absence of deadlocks
Supports partial order reduction, bitstate hashing

mtype = { request, grant };
chan ch = [1] of { mtype };

active proctype Client() {
  do :: ch!request; ch?grant; od
}

active proctype Server() {
  do :: ch?request; ch!grant; od
}

ltl liveness { [] (Client@request -> <> Client@grant) }

NuSMV

Symbolic model checker (BDD-based and SAT-based BMC)
Supports CTL and LTL
Input language describes finite-state machines

MODULE main
VAR state : {idle, busy, done};
ASSIGN
  init(state) := idle;
  next(state) := case
    state = idle : busy;
    state = busy : {busy, done};
    state = done : idle;
  esac;
SPEC AG(state = busy -> AF state = done)

TLA+ TLC Model Checker

Explicit-state model checker for TLA+ specifications
Evaluates all reachable states against invariants and temporal properties
Handles symmetry reduction via symmetry sets
Used extensively at AWS, Microsoft, and other companies for distributed protocols

State Space Reduction

Partial Order Reduction (POR)

In concurrent systems, many interleavings are equivalent. POR exploits independence of transitions: if two transitions in different processes do not affect each other, only one ordering needs to be explored.

Conditions (ample set method):

Emptiness: if the ample set is empty, the full set is used
Dependency: if a transition outside the ample set is dependent on one inside, it appears later
Invisibility: transitions in the ample set do not affect the property
Cycle: every cycle in the reduced graph contains a fully expanded state

Reduces exponential blowup to manageable sizes for many practical concurrent systems.

Symmetry Reduction

Exploit structural symmetries (e.g., identical processes) to collapse equivalent states into a single representative. Reduces state space by up to n! for n symmetric components.

CEGAR (Counterexample-Guided Abstraction Refinement)

Start with a coarse abstraction of the system
Model-check the abstraction
If property holds in abstraction, it holds in the concrete system
If a counterexample is found, check if it is spurious (infeasible in concrete system)
If spurious, refine the abstraction to eliminate it; repeat

CEGAR bridges the gap between finite model checking and infinite-state systems by automatically constructing appropriate abstractions.

         ┌──────────┐
    ┌───>│ Abstract  │──── property holds ──> Done
    │    │  Model    │
    │    └────┬──────┘
    │         │ counterexample
    │    ┌────▼──────┐
    │    │ Spurious?  │──── real ──> Bug found
    │    └────┬──────┘
    │         │ yes
    │    ┌────▼──────┐
    └────┤  Refine   │
         │ Abstraction│
         └───────────┘

Practical Considerations

State explosion mitigation strategies:

Compositional verification: verify components separately
Abstraction: remove irrelevant detail
Partial order and symmetry reduction
Bounded model checking for bug finding

When to use model checking:

Control-heavy systems (protocols, controllers, workflows)
Concurrent and distributed systems
Hardware design verification (industry standard)
Security protocol analysis

Limitations:

State explosion remains the fundamental barrier
Requires a finite (or finitizable) model
Environment modeling requires care -- over-approximation may hide bugs, under-approximation may produce false alarms

Key Takeaways

Model checking is fully automatic -- no proofs, no annotations, just a model and a property
LTL and CTL are complementary temporal logics with incomparable expressiveness
Symbolic methods (BDDs, SAT) push the scalability frontier far beyond explicit enumeration
CEGAR enables model checking of systems that are too large to explore directly
Counterexamples are the killer feature: concrete, actionable evidence of violations