Kripke structure (model checking)
From Wikipedia, the free encyclopedia
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]
- This article describes Kripke structures as used in model checking. For a more general description, see Kripke semantics.