Kripke structure (model checking)

This article describes Kripke structures as used in model checking. For a more general description, see Kripke semantics. 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 consists of a graph whose nodes represent the reachable states of the system and whose edges represent state transitions, together with a labelling function which 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-valued expressions formed from 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 a finite set of states S. a set of initial states I ⊆ S. a transition relation R ⊆ S × S such that R is left-total, i.e., ∀s ∈ S ∃s' ∈ S such that (s,s') ∈ R. a labeling (or interpretation) function L: S → 2AP. 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 ρ = s1, s2, s3, ... such that for each i > 0, R(si, si+1) holds. The word on the path ρ is the sequence of sets of the atomic propositions w = L(s1), L(s2), L(s3), ..., which is an ω-word over alphabet 2AP. 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 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 S = . I = . R = . L = .