Kripke Structures

Core Idea

A Kripke structure is the standard semantic model for temporal and modal logics, providing the mathematical framework that model checkers operate over. It consists of a set of states S, a transition relation R (which states can follow which), an initial state set I, and a labeling function L that assigns to each state the set of atomic propositions true there. Temporal logic formulas are evaluated against Kripke structures: the structure defines all possible behaviors of the system, and the model checker determines whether every behavior (or some behavior) satisfies the specification.

Explainer

A Kripke structure (named after logician Saul Kripke) is the formal mathematical object that gives meaning to temporal logic formulas. When a model checker verifies that a system satisfies a temporal specification, it is checking the specification against a Kripke structure that represents the system. The structure has four components: a finite set of states S representing possible system configurations, a set of initial states I (where the system begins), a transition relation R defining which states can follow which (R must be total — every state has at least one successor), and a labeling function L that maps each state to the set of atomic propositions true in that state.

The labeling function is the critical bridge between the system model and the specification language. Temporal logic formulas are built from atomic propositions like "mutex_held" or "buffer_full" combined with temporal operators. The labeling function tells the model checker which propositions are true in which states. For example, in a mutual exclusion protocol, state s3 might have L(s3) = {cs1, cs2}, meaning both processes are in their critical sections — a specification like AG(not (cs1 and cs2)) would fail at s3, and the model checker would report a counterexample path from an initial state to s3.

For concurrent systems, the Kripke structure of the whole system is built by composing the structures of individual components. In asynchronous (interleaving) composition, each global state is a tuple of component states, and a global transition fires when any single component takes a local step. If process A has 50 states and process B has 80 states, the composite system has up to 4,000 states — and with k processes of n states each, the composite has up to n^k states. This product construction is the formal source of the state explosion problem. Every possible interleaving of component actions is represented as a distinct path in the composite Kripke structure, which is exactly what makes model checking exhaustive but also what makes it expensive.

The evaluation of temporal formulas on Kripke structures follows a recursive definition. For CTL, the model checking algorithm works bottom-up: for each subformula, compute the set of states where it holds. EF p holds in a state s if s can reach (via transitions) some state where p holds — this is a simple backward reachability computation. AG p holds in s if every state reachable from s satisfies p. The algorithms are polynomial in the size of the Kripke structure times the length of the formula, which is efficient — the bottleneck is the size of the structure, not the complexity of the checking algorithm.

Kripke structures are intentionally abstract — they model the essential state and transitions of a system while discarding implementation details. A 1000-line C program implementing a protocol might be modeled as a Kripke structure with a few hundred states capturing only the protocol logic (who holds the lock, what messages are in flight, which phase each process is in). This abstraction is both the power of model checking (making exhaustive exploration feasible) and its limitation (the model might not faithfully represent the actual implementation). Ensuring that the Kripke structure accurately reflects the real system — or that an automatically extracted model preserves the properties of interest — is a fundamental challenge in applying model checking to practice.