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 un ensemble de propositions atomiques, c'est-à-dire des expressions booléennes portant sur des variables, des constantes et des prédicats. On note l'ensemble des parties de .
Une structure de Kripke[2],[3] est un 4-uplet où :
- est un ensemble fini d'états ;
- est un ensemble d'états initiaux ;
- est une relation de transition qui vérifie : pour tout , il existe tel que ;
- est une fonction d'étiquetage ou d'interprétation.
La condition associée à la relation de transition spécifie que chaque état doit avoir un successeur dans , 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 définit pour chaque état l'ensemble de toutes les propositions atomiques qui sont valides dans cet état.
Un chemin dans la structure est une suite d'états tels que pour tout . L'étiquette du chemin est la suite d'ensembles qui peut être vu comme un mot infini sur l'alphabet .
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
![](http://upload.wikimedia.org/wikipedia/commons/thumb/b/b6/Kripke.png/220px-Kripke.png)
Dans l'exemple ci-contre, l'ensemble de propositions atomiques est . Ici et sont des propriétés booléennes quelconques. L'état 1 contient les deux propositions, les états 2 et 3 respectivement et . L'automate admet le chemin , et le mot est la suite des étiquettes associées. Les suites d'étiquettes acceptées sont décrites par l'expression rationnelle :
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
- ↑ Kripke, Saul, 1963, « Semantical Considerations on Modal Logic », Acta Philosophica Fennica, 16 : 83-94.
- ↑ Clarke, Grumberg et Peled 1999, p. 14.
- ↑ a et b Schneider 2004, p. 45.
- ↑ 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.
- ↑ Baier et Katoen 2008, p. 20–21 et 94–95.
- ↑ Clarke, Grumberg et Peled 1999, p. 98.
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, , p. 67–96
- Saul A. Kripke, « Semantical considerations on modal logic », Acta Philosophica Fennica Fasc., vol. 16, , p. 83–94
- (en) Christel Baier et Joost-Pieter Katoen, Principles of model checking, The MIT Press, , 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 », , 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, , 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 )
- Béatrice Berard, « Vérification formelle de systèmes répartis » (consulté le )
Portail de l'informatique théorique