Kripke structure

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 [Clarke, Grumberg and Peled: "Model Checking", page 14. The MIT Press, 1999.] 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\; !\; imes\; !\; S\; ;$ where $;\; forall\; s\; !\; in\; !\; S,\; ;\; exist\; s^\text{'}\; !!\; in\; !\; S$ such that $(s,s^\text{'})\; in\; R$
* a labeling (or "interpretation") function $L:\; S\; ightarrow\; 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 all atomic propositions that are valid in "s".

ee also

* Saul Kripke
* Temporal logic
* Model checking
* Kripke semantics

References