Structure de Kripke

Soit ${\displaystyle 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 ${\displaystyle 2^{AP}}$ l'ensemble des parties de ${\displaystyle AP}$.

Une structure de Kripke[2]^,[3] est un 4-uplet ${\displaystyle M=(S,I,R,L)}$ où :

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

La condition associée à la relation de transition ${\displaystyle R}$ spécifie que chaque état doit avoir un successeur dans ${\displaystyle 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[4]. 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 ${\displaystyle L}$ définit pour chaque état ${\displaystyle s\in S}$ l'ensemble ${\displaystyle L(s)}$ de toutes les propositions atomiques qui sont valides dans cet état.

Un chemin dans la structure ${\displaystyle M}$ est une suite ${\displaystyle c=s_{1},s_{2},s_{3},\ldots }$ d'états tels que ${\displaystyle (s_{i},s_{i+1})\in R}$ pour tout ${\displaystyle i}$. L'étiquette du chemin est la suite d'ensembles ${\displaystyle w=L(s_{1}),L(s_{2}),L(s_{3}),\ldots }$ qui peut être vu comme un mot infini sur l'alphabet ${\displaystyle 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[3].

Une structure de Kripke à trois états, avec deux propositions.

Dans l'exemple ci-contre, l'ensemble de propositions atomiques est ${\displaystyle AP=\{p,q\}}$. Ici ${\displaystyle p}$ et ${\displaystyle q}$ sont des propriétés booléennes quelconques. L'état 1 contient les deux propositions, les états 2 et 3 respectivement ${\displaystyle q}$ et ${\displaystyle p}$. L'automate admet le chemin ${\displaystyle c=1,2,1,2,3,3,3,\ldots }$, et le mot ${\displaystyle 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 :

${\displaystyle \{p,q\}^{\omega }\cup (\{p,q\}^{*}q)^{\omega }\cup (\{p,q\}^{*}q)^{*}p^{\omega }}$

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[5].

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 [6].