Kripke structure (model checking)

A Kripke structure is a type of nondeterministic finite state machine proposed by Saul Kripke in 1963, 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 finite set of states $S\;$
• a set of initial states $I\subseteq S$
• a transition relation $R\subseteq S\!\times \!S\;$ where $\;\forall s\!\in \!S,\;\exists s^{'}\!\!\in \!S$ such that $(s,s^{'})\in R$
• a labeling (or interpretation) function $L:S\rightarrow 2^{AP}$

Since R is left-total, it is always possible to construct an infinite path through the Kripke structure. Thus a deadlock state has a single outgoing edge back to itself.

The labeling function L defines for each state s ∈ S the set L(s) of all atomic propositions that are valid in s. In the Kripke structure, the transition function should be complete,i.e each and every state should have transition.In other words there should not be any dead states in the graph.

See also

• Temporal logic
• Model checking
• Kripke semantics