Êtes-vous un étudiant de l'EPFL à la recherche d'un projet de semestre?
Travaillez avec nous sur des projets en science des données et en visualisation, et déployez votre projet sous forme d'application sur GraphSearch.
Concept
Structure de Kripke
Résumé
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.
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 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 dinterpré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. 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.
thumb|Une structure de Kripke à trois états, avec deux propositions.
Source officielle
À propos de ce résultat
Cette page est générée automatiquement et peut contenir des informations qui ne sont pas correctes, complètes, à jour ou pertinentes par rapport à votre recherche. Il en va de même pour toutes les autres pages de ce site. Veillez à vérifier les informations auprès des sources officielles de l'EPFL.