# Structure de Kripke

Une structure de Kripke est un modèle de calcul, proche d'un automate fini non déterministe, inventé par Saul Kripke. Elle est utilisée 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. L'existence de certains chemins dans le graphe est alors considérée comme une éventualité de réalisation de formules.

## 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. On note $2^{AP}$ l'ensemble des parties de $AP$.
Une structure de Kripke$^,$ 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 : pour tout $s\in S$, il existe $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\in S$ l'ensemble $L(s)$ de toutes les propositions atomiques qui sont valides dans cet état.
Un chemin dans la structure $M$ est une suite $c=s_{1},s_{2},s_{3},\ldots$ d'états tels que $(s_{i},s_{i+1})\in R$ pour tout $i$. L'étiquette du chemin est la suite d'ensembles $w=L(s_{1}),L(s_{2}),L(s_{3}),\ldots$ qui peut être vu comme un mot infini sur l'alphabet $2^{AP}$.
Avec cette définition, une structure de Kripke peut être vue comme un automate de Moore avec un alphabet réduit à un singleton, et dont la fonction de sortie est la fonction d'étiquetage.

## Exemple

Dans l'exemple ci-contre, l'ensemble de propositions atomiques est $AP=\{p,q\}$. Ici $p$ et $q$ sont des propriétés booléennes quelconques. L'état 1 contient les deux propositions, les états 2 et 3 respectivement $q$ et $p$. L'automate admet le chemin $c=1,2,1,2,3,3,3,\ldots$, et le mot $w=\{p,q\},q,\{p,q\},q,p,p,p,\ldots$ est la suite des étiquettes associées. Les suites d'étiquettes acceptées sont décrites par l'expression rationnelle :
    $\{p,q\}^{\omega }\cup (\{p,q\}^{*}q)^{\omega }\cup (\{p,q\}^{*}q)^{*}p^{\omega }$

## Lien avec d'autres notions

Une structure de Kripke peut être vue comme un système de transition d'états où les arcs ne sont pas étiquetés, et où en revanche les états le sont. Chez certains auteurs, les transitions des structures de Kripke sont étiquetées par des actions prises dans un ensemble fini usuellement noté Act. Lorsque cette définition est retenue, la structure sous-jacente, obtenue en omettant les actions, est appelée state graph.
Au contraire, Clarke et al. redéfinissent une structure de Kripke comme un ensemble de relations de transitions (et non plus une seule), chacune correspondant à une des étiquettes de transitions, ceci dans le cadre de la définition de la sémantique du μ-calcul modal.