Kripke structure (model checking)

A Kripke structure is a variation of the transition system, originally proposed by Saul Kripke,^[1] used in model checking^[2] 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.^{[citation needed]}