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^[1]. 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.

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

Crédit image:

ManiacParisien

licence CC BY-SA 3.0 🛈

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

• Saul A. Kripke, « Semantical analysis of modal logic. I. Normal modal propositional calculi », Zeitschrift für Mathematische Logik und Grundlagen der Mathematik, vol. 9,‎ 1963, p. 67–96

• Saul A. Kripke, « Semantical considerations on modal logic », Acta Philosophica Fennica Fasc., vol. 16,‎ 1963, p. 83–94

• (en) Christel Baier et Joost-Pieter Katoen, Principles of model checking, The MIT Press, 2008, 975 p. (ISBN 978-0-262-02649-9)

• (en) Klaus Schneider, Verification of Reactive Systems : Formal Methods and Algorithms, Springer-Verlag, coll. « Texts in Theoretical Computer Science. An EATCS Series », 2004, xiv+600 (ISBN 978-3-540-00296-3, présentation en ligne)

• (en) Edmund M. Clarke, Orna Grumberg et Doron A. Peled, Model Checking, Cambridge, MIT Press, 1999, 314 p. (ISBN 978-0-262-03270-4, présentation en ligne)

• Logique temporelle
• Logique modale
• Calculabilité
• Théorie des automates
• Machine de Turing non déterministe
• Sémantique de Kripke
• Saul Kripke

Il existe de nombreuses notes de cours, en français, sur les structures de Kripke dans le cadre de la logique ou de la vérification de programmes.

• « Logiques temporelles et vérification de programmes » (consulté le 30 juin 2012)

• Béatrice Berard, « Vérification formelle de systèmes répartis » (consulté le 30 juin 2012)

• Portail de l'informatique théorique