Structure de Kripke

Un article de Wikipédia, l'encyclopédie libre.

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.

[modifier] Définition formelle

Soit $A P$ 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.