A Kripke structure is a type of nondeterministic finite state machine used in model checking to represent the behaviour of a system. It is basically a graph whose nodes represent the reachable states of the system and whose edges represent state transitions. A labeling function maps each node to a set of properties that hold in the corresponding state. Temporal logics are traditionally interpreted in terms of Kripke structures.

Formal definition

Let AP be a set of atomic propositions, i.e. boolean expressions over variables, constants and predicate symbols.

A Kripke structure is a 4-tuple M = (S,I,R,L) consisting of

• a countable set of states (S)
• a set of initial states (I ⊆ S)
• a transition relation (R ⊆ S × S) with ∀s ∈ S (∃s‘ ∈ S ((s,s‘) ∈ R))
• a labeling (or interpretation) function (L: S → 2^AP)

The condition associated with the transition relation R states that every state must have a successor in R, which implies that it is always possible to construct an infinite path through the Kripke structure. This is an important property when dealing with reactive systems . To model a deadlock in a Kripke structure, one then simply adds an edge from the deadlock state back to itself.

The labeling function L defines for each state s ∈ S the set L(s) of atomic propositions that are valid in s.

See also

• Saul Kripke
• Temporal logic
• Model checking