Kripke structure


Kripke structure

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.

Formal definition

Let AP be a set of "atomic propositions", i.e. boolean expressions over variables, constants and predicate symbols.

A Kripke structure [Clarke, Grumberg and Peled: "Model Checking", page 14. The MIT Press, 1999.] is a 4-tuple M = (S,; I,; R,; L) consisting of
* a finite set of states S;
* a set of initial states I subseteq S
* a transition relation R subseteq S ! imes ! S ; where ; forall s ! in ! S, ; exist s^' !! in ! S such that (s,s^') in R
* a labeling (or "interpretation") function L: S ightarrow 2^{AP}

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 all atomic propositions that are valid in "s".

ee also

* Saul Kripke
* Temporal logic
* Model checking
* Kripke semantics

References


Wikimedia Foundation. 2010.

Look at other dictionaries:

  • Kripke semantics — (also known as relational semantics or frame semantics, and often confused with possible world semantics) is a formal semantics for non classical logic systems created in the late 1950s and early 1960s by Saul Kripke. It was first made for modal… …   Wikipedia

  • Structure de kripke — Une structure de Kripke est une sorte d automate fini non déterministe utilisé par exemple dans le model checking pour représenter le comportement d un système. C est un graphe orienté dont les nœuds représentent les états accessibles du système… …   Wikipédia en Français

  • Structure de Kripke — Une structure de Kripke est une sorte d automate fini non déterministe utilisé par exemple dans le model checking pour représenter le comportement d un système. C est un graphe orienté dont les nœuds représentent les états accessibles du système… …   Wikipédia en Français

  • Structure (mathematical logic) — In universal algebra and in model theory, a structure consists of a set along with a collection of finitary operations and relations which are defined on it. Universal algebra studies structures that generalize the algebraic structures such as… …   Wikipedia

  • Saul Aaron Kripke — Saul Kripke Saul Kripke. Saul Aaron Kripke (né en novembre 1940 à Omaha, Nebraska) est un philosophe et logicien américain, professeur émérite de Princeton, et professeur de philosophie à la cité universitaire de la ville de New York (City… …   Wikipédia en Français

  • Saul Kripke — Saul Kripke. Saul Aaron Kripke (né en novembre 1940 à Omaha dans le Nebraska) est un philosophe et logicien américain, professeur émérite de Princeton, et professeur de philosophie à l’université de la Ville de New York (CUNY). Il a eu une… …   Wikipédia en Français

  • Semantique de Kripke — Sémantique de Kripke La sémantique de Kripke a été proposée par Saul Aaron Kripke et est la sémantique traditionnellement associée à la logique intuitionniste et aux logiques modales. Elle est fondée sur un univers de mondes possibles, c est à… …   Wikipédia en Français

  • Sémantique de Kripke — La sémantique de Kripke a été proposée par Saul Aaron Kripke et est la sémantique traditionnellement associée à la logique intuitionniste et aux logiques modales. Elle est fondée sur un univers de mondes possibles, c est à dire que le modèle qui… …   Wikipédia en Français

  • The Structure of Scientific Revolutions — (1962), by Thomas Kuhn, is an analysis of the history of science. Its publication was a landmark event in the sociology of knowledge, and popularized the terms paradigm and paradigm shift .HistoryThe work was first published as a monograph in the …   Wikipedia


Share the article and excerpts

Direct link
Do a right-click on the link above
and select “Copy Link”

We are using cookies for the best presentation of our site. Continuing to use this site, you agree with this.