Related Directory Categories
- Kripke, Saul (3)
- Kripke, Saul (2)
Sources
Help build the largest human-edited directory on the web.
Submit a site - Become an editor
Wikipedia. Licensed under the GNU Free Documentation License.
Are you an expert in this subject? Join the discussion and share your knowledge at Wikipedia.org.
Kripke structure
From Wikipedia, the free encyclopedia
A Kripke structure is a type of nondeterministic finite state machine used in model checking to represent the behaviour 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.
A Kripke structure is a 4-tuple M = (S,I,R,L) consisting of
- a countable set of states (S)
- a set of initial states (I ⊆ S)
- a transition relation (R ⊆ S × S) with ∀s ∈ S (∃ s‘ ∈ S ((s,s‘) ∈ R))
- a labeling (or interpretation) function (L: S → 2AP)
The condition associated with the transition relation R states that every state must have a successor in R, which implies that it is always possible to construct an infinite path through the Kripke structure. This is an important property when dealing with reactive systems. To model a deadlock in a Kripke structure, one then simply adds an edge from the deadlock state back to itself.
The labeling function L defines for each state s ∈ S the set L(s) of atomic propositions that are valid in s.