Kripke structure

A Kripke structure is a variation of the transition system, originally proposed by Saul Kripke, used in model checking to represent the behavior 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.

Let AP be a set of atomic propositions, i.e. boolean expressions over variables, constants and predicate symbols. Clarke et al. define a Kripke structure over AP as a 4-tuple M = (S, I, R, L) consisting of

Since R is left-total, it is always possible to construct an infinite path through the Kripke structure. A deadlock state can be modeled by 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.

A path of the structure M is a sequence of states ρ = s₁,s₂,s₃,... such that for each i > 0, R(s_i, s_i+1) holds. The word on the path ρ is a sequence of sets of the atomic propositions w=L(s₁),L(s₂),L(s₃),..., which is an ω-word over alphabet 2^AP.

With this definition, a Kripke structure (say, having only one initial state i∈I) may be identified with a Moore machine with a singleton input alphabet, and with the output function being its labeling function.

Let the set of atomic propositions AP = {p,q}. p and q can model arbitrary boolean properties of the system that the Kripke structure is modelling.

The figure at right illustrates a Kripke structure M = (S, I, R, L), where

M may produce a path ρ = s₁,s₂,s₁,s₂,s₃,s₃,s₃,... and w = {p,q},{q},{p,q},{q},{p},{p},{p},... is the execution word over the path ρ. M can produce execution words belonging to the language ({p,q}{q})*({p})^ω∪({p,q}{q})^ω.

...
Wikipedia