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

• Machine de Turing non-déterministe
• Sémantique de Kripke
• Saul Kripke

Logique modale

Calculabilité