Kripke structure (model checking)

[citation needed] Let AP be a set of atomic propositions, i.e. boolean-valued expressions formed from variables, constants and predicate symbols.

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.

The figure at right illustrates a Kripke structure M = (S, I, R, L), where M may produce a path ρ = s1, s2, s1, s2, s3, s3, s3, ... 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})ω.

Although this terminology is widespread in the model checking community, some textbooks on model checking do not define "Kripke structure" in this extended way (or at all in fact), but simply use the concept of a (labelled) transition system, which additionally has a set Act of actions, and the transition relation is defined as a subset of S × Act × S, which they additionally extend to include a set of atomic propositions and a labeling function for the states as well (L as defined above.)

In this approach, the binary relation obtained by abstracting away the action labels is called a state graph.