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.

Définition formelle

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

Exemple

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 }}$

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

Notes et références

Notes

1. Kripke, Saul, 1963, « Semantical Considerations on Modal Logic », Acta Philosophica Fennica, 16 : 83-94.
2. Clarke, Grumberg et Peled 1999, p. 14.
3. Schneider 2004, p. 45.
4. Klaus Schneider, dans Schneider 2004, p. 12, distingue trois types de systèmes : les systèmes de transformations, les systèmes interactifs et les systèmes réactifs. Ces derniers ont l'interaction la plus souple avec l'utilisateur.
5. Baier et Katoen 2008, p. 20–21 et 94–95.
6. Clarke, Grumberg et Peled 1999, p. 98.

(en) Cet article est partiellement ou en totalité issu de l’article de Wikipédia en anglais intitulé « Kripke structure (model checking) » (voir la liste des auteurs).

Bibliographie

• 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)

Articles connexes

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

Notes de cours

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)