Structure de Kripke

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 et dont les arcs représentent les transitions entre les états. Une fonction d'étiquetage fait correspondre à chaque état un ensemble de propositions logiques vraies dans cet état. Les logiques temporelles sont généralement interprétées dans des structures de Kripke.

Définition formelle

Soit AP un ensemble de propositions atomiques, c'est-à-dire des expressions booléennes portant sur des variables, des constantes et des prédicats.

Une structure de Kripke[1] est un 4-uplet M = (S,\; I,\; R,\; L) où :

  • S\; est un ensemble fini d'états ;
  • I \subseteq S est un ensemble d'états initiaux ;
  • R \subseteq S \! \times \! S \; est une relation de transition qui vérifie : \; \forall s \! \in \! S, \; \exist s^' \!\! \in \! S tel que (s,s^') \in R ;
  • L: S \rightarrow 2^{AP} est une fonction d' étiquetage ou d' interprétation.

La condition associée à la relation de transition R spécifie que chaque état doit avoir un successeur dans R, ce qui implique que l'on peut toujours construire un chemin infini dans la structure de Kripke. Cette propriété est importante lorsque l'on traite des systèmes réactifs. Pour modéliser un interblocage dans une structure de Kripke, il suffit de faire boucler l'état d'interblocage sur lui-même.

La fonction d'étiquetage L définit pour chaque état s ∈ S l'ensemble L(s) de toutes les propositions atomiques qui sont valides dans s.

Références

  1. ↑ Clarke, Grumberg et Peled : "Model Checking", page 14. The MIT Press, 1999.

Voir aussi

Logique modale

Calculabilité


Wikimedia Foundation. 2010.

Contenu soumis à la licence CC-BY-SA. Source : Article Structure de Kripke de Wikipédia en français (auteurs)

Игры ⚽ Нужно сделать НИР?

Regardez d'autres dictionnaires:

  • 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

  • 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

  • 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… …   Wikipedia

  • 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

  • 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”